11th International Workshop on CPAchecker
(CPAchecker 2026)

The talk will briefly present two related results on bi-abductive analysis of programs with pointers, dynamic data structures, and advanced low-level pointer operations (pointer arithmetic, bitmasking on pointers, address alignment, block operations with blocks of size not known in advance, etc.). As usual with bi-abductive analyses, the results concern analysis of open programs, i.e., program fragments that do not necessarily have the main function and some verification harness. One of the results is based on a special dialect of low-level separation logic for which the approach of bi-abduction is introduced. The other result aims at avoiding the usual two-phase nature of bi-abductive analyses (one phase derives candidate function contracts, the other phase validates them) and shows that one phase suffices in many cases. The results were presented in ECOOP’22 and ESOP’25 and implemented in the tool prototypes Broom and Brush, respectively. The results are joint work with a number of researchers: L. Holík, P. Peringer, A. Rogalewicz, F. Sextl, V. Šoková, and F. Zuleger. Finally, given analysers such as Broom/Brush together with the ongoing work on correctness witnesses and their validators, the talk will also try to suggest that it is perhaps the time to introduce some competition on analysing open pointer-manipulating programs too.

Bounded model checking (BMC) finds non-terminating loops quickly: it only has to find a state that repeats at a loop head. But BMC has trouble proving termination, because it must unroll each loop until no further iteration is possible. For loops with thousands of iterations, this is not practical. In this talk, we show how to bring the idea of interpolation-based model checking from reachability to termination. First, we present the theory. We use transition invariants, which are relations between two states at a loop head that contain all sequences of loop iterations. On finite state spaces, an irreflexive and inductive transition invariant proves that the loop terminates. If a BMC query finds no repeated state, Craig interpolation gives candidate transition invariants from the refutation, and these candidates are irreflexive by construction. We extend the candidates iteratively until they reach a fixed point. Second, we show how this procedure fits into configurable program analysis (CPA). A termination CPA stores transition predicates in its abstract states. Its precision adjustment computes new predicates by interpolation and checks which of them are still transition invariants after each unrolling. Its stop operator ends the unrolling on a path when two consecutive loop-head states have the same transition invariants. Finally, we show preliminary results of our implementation in CPAchecker on the termination tasks of SV-Benchmarks.

In this talk, we present two extensions of distributed summary synthesis (DSS) in CPAchecker. First, we show how we implemented symbolic execution as a new abstract domain for DSS and discuss our evaluation results. Second, we address a source of inefficiency: currently, a block re-analyzes all of its preconditions whenever it receives a new one, even if most of them have not changed. We suggest approaches that reduce this unnecessary work using caching and subsumption checking, and show preliminary experimental evaluation of their implementations in CPAChecker.

We define a novel representation of the correctness of loops in imperative programs, called Trace Equations Systems (TEQs). The main objective is to replace the abrupt step from programs into formulas, which is inherent in Floyd/Hoare's rule for loop invariants, by a gradual transition. Our approach substitutes algorithmic inference of invariants by a database of user-defined modular and general-purpose lemmas over computation fragments as first-class objects, such as counters, array initialization, or summation of array ranges. The key technical innovation that unlocks this idea is a novel combinator called~$ race$ that exhibits the necessary structural compositionality to automate this process by first-order proof methods such as equational rewriting and resolution. Trace Equation Systems gives rise to a verification strategy based on recognizing computation fragments, assigning names to concepts of interest, including partially-resolved intermediate results, relating computation to observations of interest, such as the value of a program variable at loop exit, or the lookup in a partially initialized array. Importantly, the strategy is incremental and gives insightful feedback for partial proofs at the chosen degree of abstraction, which is in stark contrast to many state-of-the-art invariant inference techniques. We show how known loop acceleration techniques or program transformations for verifiability can be expressed as equations or implications in the database. We implement and evaluate the approach, demonstrating its effectiveness and efficiency on variety of benchmarks.

TBA

Debugging software systems is a tedious and time-consuming activity, which includes reproduction of the observed errors, inspecting log files, usage of interactive debuggers, and running tests - all that is done with the goal of identifying a root cause. The process of debugging is even more challenging in the case of large systems with long computations, where programs (and test suites) may run for hours. We introduce a debugging workflow that combines dynamic analysis with directed unit tests, and present ACF, an infrastructure for automating this workflow. Dynamic analysis collects runtime data about procedure calls, their argument values, and relevant program states during execution of a target system. Tests use the recorded values as inputs. We have implemented the ACF infrastructure for C/C++ programs on top of LLVM. Our experiments with real-world systems indicate that ACF can help developers to isolate specific inputs causing an error, thus simplifying the process of locating faulty statements. In this talk, we will also discuss how CPAchecker could be used together with ACF in practice, for tasks such as discovery of errors and validation.

In this talk we discuss topics that are currently relevant for the development of CPAchecker. One focus are tests and CI, for which some recent restructurings and improvements are presented, but more effort is needed for integration tests for some areas. Further topics are the minimal Java version that CPAchecker requires, in particular if and when to raise it to Java 25, and potential guidelines for LLM usage in CPAchecker development. Feedback and suggestions from developers on these and other topics is welcome!