CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification

Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee

This work is accepted at ASE 2023. A preprint and the publisher's version of this article are available for you to download.


Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.

Demonstration video:

Tool and Reproduction Information

A reproduction package of this work is available on Zenodo (DOI). The SVN repository (corresponding git commit) contains the revision of CPA-DF used in the evaluation.


Full Results

The experimental results reported in the paper can be seen in the interactive tables below. You can click on the cells in the status columns to see the corresponding log output and use the respective tabs to show various plots.