CPAchecker 2.3 with Strategy Selection

CPAchecker  [10] is a flexible framework for automatic software verification based on the concept of Configurable Program Analysis (CPA) [9]. Abstract domains needed by a verification approach are represented as CPAs, and multiple CPAs can be combined in a modular fashion to achieve synergy. CPAchecker provides basic functionalities for program analysis, such as tracking the control flow or callstack, as standalone CPAs, which facilitate the implementation of new analyses. Through its modular architecture, a rich collection of verification algorithms [7, 12, 14, 24] has been implemented in CPAchecker, and its flexibility and extensibility have been evidenced by many research projects.

Operating Platform. CPAchecker is platform-independent as it is written in Java. However, its default SMT solver MathSAT5 [17] is bundled only for Linux. Thanks to the versatility of the used library JavaSMT [23], a different SMT solver can be chosen on other platforms.

Witnesses. CPAchecker  produces correctness and violation witnesses for all properties where the corresponding witness type is already defined by the community. These are exported in the established GraphML format [4, 5] as well as in the new YAML format that is introduced with SV-COMP 2024.

Strategy selection based on the property to verify and program structure (New components since the last published system description [19] are marked in boldface. ‘+’ and ‘;’ denote component composition and sequential execution, respectively.)

Full size image

To effectively solve the verification tasks from the heterogeneous benchmark set used in the competition, we need different verification strategies. Given a verification task, we select a suitable strategy with a two-level approach according to the property of the task and the structure of the program. A strategy could be a sequential portfolio of different verification techniques, each of which is assigned a time limit that is determined with expert knowledge. Figure 1 shows the selection procedure. The first-level selection is based on the property of the verification task. If the property is among memory safety, no-dataraces, no-overflows, or termination, a dedicated strategy is immediately assigned to solve the task. If the property is reachability safety, we further distinguish the program structure of a task into six classes by a set of carefully picked features, and a tailored strategy is invoked for each class. The details for each property and program structure are given below.

Memory Safety. Memory safety is checked by an unbounded analysis based on symbolic memory graphs (SMGs) [20]. It utilizes symbolic execution [13] to reason over non-concrete values, enabling us to verify the safety of low-level memory operations. The graph-based approach allows us to not only represent heap memory efficiently, but also to abstract linked memory structures (e.g., linked lists) that are created with low-level memory operations.

No Data Race. Data races are checked with a combination of value analysis (Val) [14], the thread handling from our concurrency analysis [8], and a CPA that tracks read and write accesses to memory locations. We perform partial order reduction (POR) [25] over thread-local memory accesses to improve performance.

No Overflow. Overflows are checked with a CPA that adds additional constraints for overflow detection and a bit-accurate predicate abstraction (PredAbs) [7]. For recursive tasks we add block-abstraction memoization (BAM) [21, 27], which summarizes the input-output behavior of recursive functions.

Termination. Our termination strategy consists of two techniques. The first technique transforms liveness to a safety property [26]. With a combination of predicate and value analyses we check whether there exists some program state at a loop head that can be visited twice. If the program is recursive or the analysis reaches a time limit of 300 s, we switch to the second techniques, which uses ideas first implemented in Terminator  [18]: We apply CPAchecker ’s predicate-based reachability analysis to detect potentially non-terminating program executions, called candidate lassos. A lasso consists of a stem (a finite program path) that is followed by a loop (a finite program path that describes a syntactic cycle in the program). Found candidate lassos are analyzed with the library LassoRanker [24] to synthesize termination and non-termination arguments. If a non-termination argument is found for at least one candidate lasso, violation of the termination property is reported. Otherwise, the analysis claims the program as terminating.

Reachability Safety. For the reachability of an error location, we tailor our verification strategy based on the structure of the program. If the program contains a recursive function, we apply block-abstraction memoization [21, 27] in combination with value analysis (Val) and predicate abstraction (PredAbs). If the program is multi-threaded, a concurrency analysis [8] that relies on binary decision diagrams (BDD) is applied. We set an upper limit of five threads for the analysis, and if this threshold is surpassed, the analysis is aborted. For non-recursive and single-threaded programs, we assign one of the four verification strategies in Fig. 1 according to the following structural features: the number of loops and whether the program contains non-integer data types, such as floating-point variables, arrays, or composite data structures [3]. The four strategies are all based on sequential combinations [19] of various bit-precise analyses with different time limits. For loop-free programs, we apply bounded model checking (BMC) [16] with a fallback to PredAbs [22]. For programs with a single loop, we apply a sequence of symbolic execution [13], Val [14], PredAbs [11], interval-based data-flow analysis (DF) [2], and interpolation-based model checking (IMC) [12]. For programs with multiple loops and non-integer data types, we apply Val and k-induction  [6]. For all other programs, i.e., those with multiple loops but without non-integer data types, we apply a sequential portfolio of symbolic execution, Val, PredAbs, DF, and k-induction.

CPAchecker with strategy selection performed well in SV-COMP 2024 [1], winning the second place in category Overall and the first place in category FalsificationOverall. Notably, it produced 17 968 correct and confirmed results, more than any other participant, and outperformed the winner in category Overall by 32 %. CPAchecker is also robust: More than 96 % of its correct results were confirmed by witness validators, and it produced only 17 wrong results (0.06 % of all tasks).

CPAchecker won the third place in category ReachSafety by using various analyses orchestrated by strategy selection. For programs with non-integer data types, k-induction was the most effective analysis. In programs with loops, most alarms were found by symbolic execution, and most proofs were delivered by value analysis and predicate abstraction.^{Footnote 1}

The only categories without a medal for CPAchecker were Termination, ConcurrencySafety, and MemSafety. In particular, all wrong results in the category MemSafety are due to imprecise abstractions of nested lists. To alleviate them, we intend to improve the precision of our list abstraction and incorporate SMT-based array abstraction, which would make CPAchecker more effective in this category. To improve the termination analysis, we plan to make the analyses more cooperative and carry over partial proofs in the sequential combination. Additionally, CPAchecker needs improvements for finding invariants with quantifiers, which mainly affects verification tasks with large arrays.

SV-COMP 2024 ran CPAchecker version 2.3 [15] on all categories with C programs. It runs on a standard GNU/Linux system with a Java 17 compatible runtime environment. To start CPAchecker, execute the following command:

For programs assuming a 64-bit memory model, append the argument -64 to the command line. At the end of the execution, the verification result is printed to the console output and the witnesses are written to the files witness.graphml and witness.yml in the directory output/.

Note that the configuration -svcomp24 is optimized specifically for the resource limits used in SV-COMP (15 GB of RAM and 15 min CPU time per task). For other use cases (e.g., with less RAM or a different time limit), please apply a different configuration (e.g., -default) and adjust the memory consumption with the command-line option -heap as described in the documentation.

More than 100 developers have contributed to CPAchecker, mainly from LMU Munich, TU Darmstadt, U Paderborn, U Passau, TU Prague, U Oldenburg, TU Vienna, ISP RAS, and several other universities and institutes. We would like to thank all contributors for their investment in CPAchecker. A complete list and more information about the project is available at https://cpachecker.sosy-lab.org. A list of bugs that CPAchecker found in the Linux kernel is also available.