A preprint of this article is available for you to download. The published paper is available from SpringerLink.
Block summarization is an efficient technique in software verification to decompose a verification problem into separate tasks and to avoid repeated exploration of reusable parts of a program. In order to benefit from abstraction at the same time, block summarization can be combined with counterexample-guided abstraction refinement (CEGAR). This causes the following problem: whenever CEGAR instructs the model checker to refine the abstraction along a path, several block summaries are affected and need to be updated. There exist two different refinement strategies: a destructive in-place approach that modifies the existing block abstractions and a constructive copy-on-write approach that does not change existing data. While the in-place approach is used in the field for several years, our new approach of copy-on-write refinement has the following important advantage: A complete exportable proof of the program is available after the analysis has finished. Due to the benefit from avoiding re-computations of missing information as necessary for in-place updates, the new approach causes almost no computational overhead overall. We perform a large experimental evaluation to compare the new approach with the previous one to show that full proofs can be achieved without overhead.
We performed an extensive experimental evaluation to compare two different refinement approaches for BAM. We used our framework CPAchecker (in revision 28001) and the SV benchmark suite for comparison.
A table listing all experimental results can be found here (CSV). Please note that the table is big and may slow down your browser.
We assume that your machine meets the following or similar requirements:
Please make sure that the following components are available in a local directory $BASE:
To execute our experiments with the model checkers, run:
cd $BASE/cpachecker
scripts/benchmark.py ../bam-ip-cow.xml
The results for CPAchecker will be in $BASE/cpachecker/test/results
To visualize the created results, you can use the tool table-generator:
scripts/table-generator.py \
test/results/bam-ip-cow.$DATE.results.predbam-ip.xml.bz2 \
test/results/bam-ip-cow.$DATE.results.predbam-cow.xml.bz2 \
test/results/bam-ip-cow.$DATE.results.valuebam-ip.xml.bz2 \
test/results/bam-ip-cow.$DATE.results.valuebam-cow.xml.bz2
After executing all these steps, you should have produced the data provided above yourself. Feel free to play around with the tools some more.