Precision Reuse for
Efficient Regression Verification
Abstract
Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions.
The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are reasonably small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems created from 62 Linux kernel device drivers with 1119 revisions.
The webpage of our ESEC/FSE Evaluated Artifact Collection contains more details about the verification tasks that we used in our experimental evaluation.
Supplementary Data
The supplementary archive (327 MB) contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker. The archive was built from the branch “trunk” with revision 8112 of the CPAchecker repository. The following (relevant) files are in this archive:
| config/ | The CPAchecker configuration files that we used in the experiments. |
| programs/ | The driver revisions. |
| our-results/ | Our raw results, including log files and tables (see also below). |
| *.xml | The input files for our benchmarking script:
|
Full Results
The full results for all drivers and all (six) specifications can be found in the following tables:
Raw Results
The raw result tables are available here:
- Raw results for explicit analysis (all revisions)
- Raw results for explicit analysis (each 4th revision)
- Raw results for predicate analysis (all revisions)
- Raw results for predicate analysis (each 4th revision)
You can click on the cells in the status columns in these tables to see the CPAchecker log file. Clicking on the column headings (e.g., “Analysis CPU Time”) will produce a graph (this requires JavaScript to be enabled).
The corresponding CSV files can be found in the our-results directory of the supplementary archive.
Reproducing the Results
In order to reproduce the results, download the supplementary archive and follow these steps. Linux is required to run the experiments because the SMT solver used by CPAchecker (MathSAT5) is only available for Linux. CPAchecker requires that the amount of memory used for the Java heap is set according to the memory of your machine. If this parameter is higher than the available memory, the JVM will not start. For the results in the paper, a value of “10000m” was used; the whole process (including the RAM that was used by the SMT solver) was limited to 15 GB of RAM.
How to run CPAchecker on a set of programs
CPAchecker can be executed with different configurations on a set of programs by using the benchmarking script (scripts/benchmark.py). You can find the input file (*.xml) for the benchmarking script in the root folder of the supplementary archive.
- The Java heap size limit is defined in the benchmark definition XML files.
If you have less than 16GB of RAM (or if not enough memory is free on your machine), you need to adjust this number by changing the following line in the file:
<option name="-heap">10000m</option>
- Run the benchmark script scripts/benchmark.py with the benchmark definition file. Example:
scripts/benchmark.py bench-explicit-all.xml
- The results (log files and data) will be placed in the directory test/results/.