Replication package for article 'Parallel Program Analysis on Path Ranges'

This Replication package contains all the results for the article "Parallel Program Analysis on Path Ranges" Abstract. Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so called {\em path ranges}, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run {\em different} analyses on different program parts. We have implemented this generalization on top of the tool \textsc{CPAchecker} and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelisation of the verification task, but also needs a form of work stealing (between analysis) as to become efficient.