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.