CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification
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%.
Po-Chun Chien (ORCID, DBLP) is a doctoral researcher at SoSy-Lab, LMU Munich, and is a part of the DFG research training group ConVeY. Prior to joining SoSy-Lab, he received his B.S. and M.S. degree from National Taiwan University.
His research focuses on formal verification and optimization of computational systems, including software programs and VLSI circuits. He has developed and contributed to several open-source verification tools, including CPAchecker, Btor2C, CoVeriTeam, and ABC.
Mon 11 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Can ChatGPT Support CPAchecker with Useful Loop Invariants?|
Cedric Richter Carl von Ossietzky Universität Oldenburg / University of Oldenburg
|CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification|
Po-Chun Chien LMU MunichPre-print Media Attached File Attached
|A Unifying Approach for Control-Flow-Based Loop Abstraction|
Marian Lingsch-Rosenfeld LMU MunichLink to publication File Attached
|Backward Bounded Model Checking in CPAchecker|
Bas Laarakker University of Amsterdam