Dirk Beyer, Andreas Holzer, Michael Tautschnig, and Helmut Veith
It is well known that model checkers can generate test inputs as witnesses for reachability specifications (or, equivalently, as counterexamples for safety properties). While this use of model checkers for testing yields a theoretically sound test-generation procedure, it scales poorly for the computation of complex test suites with large sets of test goals, because each test goal requires a costly call to the model checker. We represent test goals as automata and exploit relations between automata in order to reuse existing reachability information for the analysis of subsequent test goals. Exploiting the sharing of subautomata in a series of reachability queries, we achieve considerable performance improvements over the naive approach. We show the practical use of our multi-goal reachability analysis in a predicate-abstraction-based test-input generator for the test-specification language FQL.
The supplementary archive contains all data from our experiments. The following files are in this archive:
...folders that contain the very detailed logfiles of each verification run.
For obtaining CPAchecker, we refer to our public repository. To install CPAchecker, run the following commands:
svn co -r ??? https://svn.sosy-lab.org/software/cpachecker/trunk cpa-tiger
cd cpa-tiger
ant
To then run a benchmark with, e.g., our first configuration, run: ... ??? ...
scripts/cpa.sh -heap 12500M -noout -explicitAnalysis -stats test/programs/benchmarks/ntdrivers-simplified/cdaudio_simpl1_unsafe.cil.c
The result tables of the figures in the paper are available here:
You can click on the cells in the status columns in these tables to see the output of CPAchecker.