Dieses Kapitel bietet einen detaillierten Einblick in die Architektur und die Validierungsmöglichkeiten von CPAchecker 4.0, einem leistungsstarken Werkzeug zur automatischen Softwareüberprüfung und Zeugenvalidierung. Der modulare Aufbau des Tools, der auf dem Konzept der konfigurierbaren Programmanalyse (CPA) beruht, ermöglicht die nahtlose Integration verschiedener Analysen und die Handhabung unterschiedlicher Anwendungsfälle, von der Zeugenvalidierung bis hin zur Testfallgenerierung. In diesem Kapitel wird untersucht, wie CPAcheckers stärkender Operator den Informationsaustausch zwischen verschiedenen CPAs erleichtert und die Anpassung bestehender Analysen für die Validierung von Zeugen ermöglicht. Er geht den Herausforderungen nach, die es mit sich bringt, Eingabeprogramme mit ihren internen Repräsentationen in Verbindung zu bringen, und wie CPAchecker diese Probleme angeht, insbesondere für Zeugen, die ausschließlich über das Eingabeprogramm definiert werden. In diesem Kapitel wird auch der Algorithmus-Auswahlprozess des Tools diskutiert, der Zeugentyp, Eigentum und Programmmerkmale berücksichtigt und einen detaillierten Überblick über Validierungsansätze für verschiedene Kategorien bietet, einschließlich Korrektheitszeugen, Erreichbarkeitssicherheit und Verletzungszeugen. Darüber hinaus hebt er die Leistung von CPAchecker in Wettbewerbsumgebungen wie SV-COMP 2025 sowie seine Stärken und Schwächen in verschiedenen Validierungskategorien hervor. Das Kapitel bietet auch Einblicke in die Einrichtung, Konfiguration und die Beiträge der Entwickler des Tools, was es zu einer unverzichtbaren Lektüre für diejenigen macht, die sich für fortgeschrittene Software-Verifikationstechniken interessieren.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
CPAchecker is a tool for software verification, witness validation, and test-case generation, based on the concept of configurable program analysis. One of its main applications is to validate correctness and violation witnesses in versions 1.0 and 2.0. The witness validation is achieved by strengthening a selection of verification algorithms using the information from the witness. Due to the modular approach of CPAchecker, extending its verification analyses for witness validation can be easily done. Similar to CPAchecker ’s verification approach, witness validation uses a selection of analyses dependent on the witness type, the specification, and program features. To validate correctness witnesses, CPAchecker uses k-induction and predicate abstraction to verify that the invariants from the witness hold and the correctness of the program can be proven. To validate violation witnesses, CPAchecker uses predicate abstraction, value analysis, SMGs, and BDDs. CPAchecker ’s many verification algorithms make it a versatile and successful tool for witness validation.
Hinweise
M. Lingsch-Rosenfeld—Jury member.
1 Software Architecture
CPAchecker [13] is a tool for automatic software verification, witness validation, and test-case generation. It is possible for it to cover these different use-cases due to its modular architecture, based on the concept of Configurable Program Analysis (CPA) [12]. Each CPA represents information relevant to an analysis, for example an abstract domain, control-flow information, or an automaton, and can be combined with other CPAs in a modular manner. Exchanging information with other CPAs is done through a well-defined interface called the strengthening operator, which is used to incorporate information from one abstract state into the another. This modular approach allows any analysis, of which many exist [2, 4, 5, 7, 8, 15, 16], to be used for witness validation. The information from the witness can be encoded as a CPA, simplifying the adaptation of existing analyses for witness validation. One major challenge for witness validation is relating the input program to its internal representation as a control-flow automaton (CFA). In particular, this challenge occurs when validating witnesses in version 2.0, which are defined purely on the input program [1]. CPAchecker analyses such witnesses by transparently keeping track of the abstract-syntax-tree elements generated during parsing and their correspondence to the CFA nodes and edges.
Fig. 1.
Algorithm selection based on the witness type, property, and program
2 Validation Approach
When participating as a verifier, CPAchecker uses different verification algorithms [3, 6], since each has specific strengths and supports different properties. To validate witnesses, we choose only the most mature analyses and adapt the selection process to consider the witness type (violation or correctness), specification, and program features for the selected analyses. Figure 1 shows the selection process. The chosen verification algorithm is strengthened with the information from the witness. The analyses and how they interact with the witness are described in the following sections for all validation categories.
Anzeige
2.1 Correctness Witnesses
Validation of correctness witnesses is based on strengthening the chosen analysis using the invariants provided by the witness. Additionally, the invariants are added as proof-goals in order to validate their correctness.
Reachability Safety.CPAchecker uses one of its best-performing and mature analyses for reachability safety, k-Induction [7] augmented with invariants from the witness. First the invariants are matched to their corresponding nodes of the control-flow automaton (CFA). For witnesses 1.0 we do this by a reachability analysis only dependent on the control-flow. For witnesses 2.0 we directly match the location of invariants to their corresponding CFA nodes. Afterwards, k-Induction first verifies that the invariants are correct and then uses them to prove the safety property, while increasing k as necessary. This means that all invariants in the witness need to be k-inductive for some k in order to be validated.
No Overflow. To validate witnesses for proofs showing the absence of overflows, CPAchecker uses predicate abstraction [14]. The information in the witness is encoded using an invariant-injection automaton, which is traversed simultaneously to the state-space exploration and strengthens the analysis. Recursive programs are handled by block-abstraction memoization (BAM) [9, 10, 24, 26], which summarizes the input-output behavior of recursive functions.
2.2 Violation Witnesses
Due to the modular nature of CPAchecker, any analysis, except for the validation of non-termination witnesses (see below), can easily be combined with an automaton, represented as a CPA, that restricts the state space and strengthens the analysis with assumptions. The automaton is based on the witness and guides the analysis towards the violation by exploring it simultaneously to the state-space. We restrict the state space by avoiding any transition that does not match the witness. For example, if the then branch is desired by the witness, then the analysis stops the exploration of the else branch. We strengthen the analysis by adding the assumptions to the abstract state. The assumptions are added through a common interface, the strengthening operator [8], which each analysis needs to implement to successfully make use of the information.
Anzeige
Termination. To validate a non-termination witness, we need to show that (1) the stem of the witness can reach the recurrence condition and that (2) whenever a state fulfills the recurrence condition, it returns to a state at the loop-head fulfilling the recurrence condition. Both of these checks are expressed as reachability analyses performed by predicate abstraction [14].
No Data Race. To validate a witness showing that there is a data race, we use an analysis based on value analysis [16] and predicate abstraction [14]. The value analysis uses the assumptions in the witness to determine additional concrete values to be tracked. The predicate abstraction adds the assumptions to the path formula to compute what predicates are valid in the successor state. The same strengthening is done whenever information from the witness needs to be added to either the value analysis or predicate abstraction for any other property.
Memory Safety. For memory safety, a combination of value analysis and symbolic memory graphs (SMGs) is used to explore the state-space while keeping track of the memory structure. In this case, the assumptions in the witness are used to strengthen the abstract state of the value analysis.
Reachability Safety. Predicate abstraction [14] is used to validate violation witnesses for reachability safety. It is aided by BAM [10, 24, 26] for tasks with recursive functions. The assumptions inside the witness are used to strengthen the predicate abstract state. If the task contains concurrency, an analysis based on BDDs [11, 18] is used, which currently ignores the assumptions in the witness.
No Overflow. To validate no-overflow violation witnesses, predicate abstraction [14] is used. The assumptions are used to strengthen the predicate abstract state. To handle tasks with recursion we add BAM [10, 24, 26].
3 Strengths and Weaknesses
CPAchecker validator performed well in SV-COMP 2025 [19], consistently ranking in the top three in almost all categories with a well-defined witness format, the only exceptions being validation of handcrafted violation witnesses in version 2.0, validation of software-systems correctness witnesses in version 1.0, and validation of reach-safety and no-overflow violation witnesses in version 1.0. In particular, it is one of the only three validators participating in all categories for which a witness format exists, together with UAutomizer and MetaVal. In general, CPAchecker performed similarly when validating witnesses in version 1.0 and in version 2.0, since both are encoded in the same manner as a CPA to combine them with the verification analyses.
Notably CPAchecker performed best in the validation of correctness witnesses, but lagged behind other tools when validating violation witnesses. This is due to CPAchecker using primarily the predicate analysis for validation, which is better in finding proofs than bugs. In general, since the analyses used for validation are the same as for verification, only strengthened with the witnesses, they have the same strengths and weaknesses.
We do not use the parallel portfolio of different analyses that boosts CPAchecker 4.0 as a verifier, we rather select one mature analyses, in order to increase the confidence in the validation result. In the future, a portfolio of other mature analyses could be used, improving the performance without compromising the confidence in the results.
4 Setup and Configuration
CPAchecker validator in version 4.0 [20] was used in SV-COMP 2025. It runs on any system with a Java 17 compatible runtime environment, though its default SMT solver MathSAT5 [22] is bundled only for Linux. For platforms other than GNU/Linux, we recommend using the provided container image [21]. To validate a witness using CPAchecker, execute the following command:
SV-COMP uses a timelimit of 900 s for correctness witnesses and 90 s for violation witnesses, though it will work with other/no time limits. Replace
by
for programs that assume a 64-bit memory model. More information on how to run CPAchecker is available on its website https://cpachecker.sosy-lab.org and tutorial paper [2].
5 Project and Contributors
CPAchecker validator builds upon existing verification algorithms with additional support for handling witnesses. The success of CPAchecker is the result of contributions from over 100 developers, primarily from institutions such as LMU Munich, TU Darmstadt, University of Paderborn, University of Passau, TU Prague, University of Oldenburg, TU Vienna, ISP RAS, and numerous other universities and research institutes. We extend our utmost gratitude to all contributors to CPAchecker which made it possible to have such a successful validator. A complete list of contributors and further details about the project can be found at https://cpachecker.sosy-lab.org.
Data-Availability Statement. The tool is available at https://cpachecker.sosy-lab.org and the version used in SV-COMP 2025 is archived at Zenodo [20].
Funding Statement. This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) – 378803395 (ConVeY) and 496588242 (IdeFix).
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
by
for programs that assume a 64-bit memory model. More information on how to run CPAchecker is available on its website https://cpachecker.sosy-lab.org and tutorial paper [2].
