Replication package for article 'Parallel Program Analysis via Range Splitting'

Abstract. Ranged symbolic execution was proposed to scale symbolic execution by splitting the task of path exploration onto several workers. The split is conducted along path ranges which – simply speaking – describe sets of paths. Workers can then explore path ranges in parallel. In this paper, we propose ranged analysis as the generalization of ranged symbolic execution to arbitrary program analyses. This allows us to not only parallelize a single analysis, but also run different analyses on dif- ferent ranges of a program. Besides this generalization, we also provide a novel range splitting strategy along loop bounds, complementing the ex- isting random strategy of the original proposal. We implemented ranged analysis within the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. The evaluation in particular shows the superiority of loop bounds splitting over random splitting and that com- positions of ranged analyses can solve analysis tasks which none of the constituent analysis alone can solve. The artifact contains a file REAME.HTML, that contains all the information needed