CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification
This work is accepted at ASE 2023.
A 
preprint
and the 
publisher's version
of this article are available for you to download.
Abstract
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: https://youtu.be/l7UG-vhTL_4
Tool and Reproduction Information
A reproduction package of this work is available on Zenodo
(
).
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.