10th International Workshop on CPAchecker
(CPAchecker 2025)

The talk will present a simple, yet effective program verification technique that combines symbolic execution with implicit predicate abstraction and CEGAR. The technique can prove correctness of many programs that are beyond the reach of the standard symbolic execution because their symbolic execution tree is prohibitively large or even infinite. The technique has been implemented in the software model checker Kratos. Experimental evaluation shows that the technique decides correctness of some programs that were decided neither by the standard symbolic execution nor by IC3 with predicate abstraction (all implemented in Kratos). A preliminary version of the technique was introduced at FMCAD 2024.

In this talk, we give a short overview of our past, current, and future work on distributed summary synthesis (DSS). We present a framework that allows to synthesize summaries for programs parts in parallel. This is achieved by subdividing the program into coherent code blocks that can be analyzed independently. Currently, all this happens inside CPAchecker. While we want to improve DSS inside CPAchecker, we also plan to extend DSS using off-the-shelf verifiers. We discuss the challenges and benefits of DSS, as well as the current state of our implementation.

TBA

TBA

Software verification witnesses are a machine-readable format to represent the results of a verification run. They can be used to independently validate the verification result, exchange information between different tools, and to provide feedback to the user. In this talk, we will give an overview of the witness format 2.0 with some of the extensions for format 2.1. We will also take a look at how CPAchecker exports and validates witnesses.

Lately new extensions of the witness format 2.0 were presented for termination and non-termination properties. CPAchecker could validate non-termination witnesses version 1.0. In this talk, I present adaptation of CPAchecker to validate non-termination and termination witnesses for witness format 2.1.

Software verifiers have become increasingly effective at the task of proving the correctness of software with respect to a formal specification. Yet, without a formal specification, a software verifier alone can neither certify the correctness of software nor find novel software bugs. Large language models (LLMs) have the potential to automate the process of generating formal specifications by harnessing natural information of the program such as signatures, names, comments or documentations. However, it is unclear whether existing LLMs can reliably generate correct and useful specifications that would enable software verifiers to detect software bugs. In this talk, we investigate this question by introducing a novel approach for automatic bug detection that combines LLMs and software verifiers. The LLM generates likely specifications that are then verified with a software verifier. Any specification violation is then reported as a potential bug. We evaluate our approach for finding bugs in Python programs. Our investigation shows that software verifiers supplemented with LLM-generated specifications are more effective in finding difficult software bugs than recent testing based approaches.

TBA

TBA

Since the last workshop CPAchecker's repository was migrated to Git. We look back on the decisions made on the last workshop and discuss whether we want to change any of the existing policies. Furthermore, we present and discuss finished, ongoing, and future modernizations of the code base of CPAchecker with respect to the adoption of new Java features. And we will discuss and decide when CPAchecker will start requiring Java 21.