Published October 12, 2022 | Version Version for Artifact Evaluation
Other Open

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

  • 1. University of Oldenburg
  • 2. TU Darmstadt

Description

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!

Files

ranged-analysis-execution-artifact-fase23.zip

Files (2.0 GB)

Name Size Download all
md5:8f48e2747b90440f53c66455539c9741
272 Bytes Download
md5:79b386b80bfc750185da7d231880c43d
2.0 GB Preview Download