Parallel Program Analysis on Path Ranges

TL;DR

Ranged program analysis extends the concept of path range parallelism to arbitrary analyses by splitting the program execution space into path ranges and running different analyses on each range. It introduces a range reduction CPA and a splitting strategy, plus a witness joining mechanism to compose partial results into a full program verdict, with work stealing to balance workload across analyses. Empirical evaluation on SV-COMP benchmarks shows that combining path-range partitioning with both same and different analyses can increase the number of solved tasks, especially when leveraging work stealing, while maintaining sound witness validation. The approach is implemented in CPA-checker and Co-Veri-Team and demonstrates practical gains for cooperative verification and scalable software analysis.

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 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 different analyses on different program parts. We have implemented this generalization on top of the tool 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 analyses) as to become efficient

Figures (14)

• Figure 1: Example program, its CFA, and a shortened execution tree
• Figure 2: Conceptual overview of ranged program analysis for two ranged analyses
• Figure 3: Application of range reduction on the running example of \ref{['fig:exCFA']}
• Figure 4: For given test $\tau_2=\{x\mapsto0\}$ and our example program from Fig. \ref{['fig:exCFA']}, correctness witnesses for ranged analysis on [$\pi_{^{_\bot}}, \pi_{\tau_2}$] produced by predicate abstraction (green highlighted invariants), correctness witness for ranged analysis on [$\pi_{\tau_2}, \pi^{_{\top}}$] produced by value analysis (red highlighted invariants) and correctness witness generated by Alg.~\ref{['alg:joinWit']} (black invariants) when given these two witnesses and our example program.
• Figure 5: Ranged analysis with work stealing, where Ranged Analysis 1 completes the verification of both ranges