CPA-DF

Beyer, Dirk ; Chien, Po-Chun und Lee, Nian-Ze (2023): CPA-DF. A Tool for Configurable Interval Analysis to Boost Program Verification. 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), Echternach, Luxembourg, 11. - 15. September 2023. Bissyandé, Tegawendé F. (Hrsg.): In: 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), Piscataway: IEEE. S. 2050-2053

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

• Dokumententyp: Konferenzbeitrag (Paper)
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISBN: 979-8-3503-2996-4 ; 979-8-3503-2997-1
• Ort: Piscataway
• Sprache: Englisch