Abstract We present Nacpa, a meta-verifier based on parallel portfolio and native compilation of backend verifiers. Nacpa does not implement any software analyses itself, but uses the Java-based CPAchecker as off-the-shelf verification backend in different configurations; each called as a separate, external process. To avoid the overhead of starting the Java Virtual Machine multiple times and to improve the run time on fast-to-solve tasks, we created a natively compiled version of CPAchecker for Nacpa. Nacpa is a conceptually simple framework, yet proves to be competitive in SV-COMP 2025.

Abstract We present CPA-Daemon , a microservice for continuous software verification of C code. CPA-Daemon provides full access to the verifier CPAchecker , but adds a clear network interface based on gRPC that abstracts from three different modes of execution: (1) running CPAchecker in a separate JVM, (2) running CPAchecker as a native executable compiled with GraalVM, and (3) running CPAchecker in a shared, continuously-running JVM. The last two are novel execution modes that greatly improve the response time of verification in different verification scenarios and enable the seamless integration of CPAchecker as an engine in other verification tooling. Our comparative evaluation shows that CPA-Daemon reduces the response time on small verification tasks down to 17%, and that it can reduce the response time of existing cooperative verification techniques down to 70%. While our implementation focuses on CPAchecker , the conceptual ideas are of general nature and can serve as a solution for other verification tools that face similar JVM-specific issues. CPA-Daemon is open source and available at https://gitlab.com/sosy-lab/software/cpa-daemon .

Abstract This tutorial provides an introduction toCPAcheckerfor users.CPAcheckeris a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking,Impact, interpolation-based model checking,k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases forCPAcheckerin formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases ofCPAcheckerfor test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge ofCPAcheckeris not required. This tutorial and user guide is based onCPAcheckerin version 3.0. This user guide’s latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php .

Abstract Software is ubiquitous in the digital world, and the correct function of software systems is critical for our society, industry, and infrastructure. While testing and static analysis are long-established techniques in software-development processes, it became widely acknowledged only in the past two decades that formal methods are required for giving guarantees of functional correctness. Both academia and industry worked hard to develop tools for formal verification of software during the past two decades, with the result that many software verifiers are available now (for example, 59 freely available verifiers for C and Java programs). However, most software verifiers are challenging to find, install, and use for both external researchers and potential users. FM-Weck changes this: It provides a fully automatic, zero-configuration container-based setup and execution for more than 50 software verifiers for C and Java. Both the setup requirements and execution parameters of every supported verifier are provided by the tool developers themselves as part of the FM-Tools metadata format that was established recently and was already used by the international competitions SV-COMP and Test-Comp. With our solution FM-Weck, anyone gets fast and easy access to state-of-the-art formal verifiers, no expertise required, fully reproducible.

We present CoVeriTeam GUI, a No-Code web frontend to compose new software-verification workflows from existing analysis techniques. Verification approaches stopped relying on single techniques years ago, and instead combine selections that complement each other well. So far, such combinations were---under high implementation and maintenance cost---glued together with proprietary code. Now, CoVeriTeam GUI enables users to build new verification workflows without programming. Verification techniques can be combined through various composition operators in a drag-and-drop fashion directly in the browser, and an integration with a remote service allows to execute the built workflows with the click of a button. CoVeriTeam GUI is available open source under Apache 2.0: https://gitlab.com/sosy-lab/software/coveriteam-gui

Abstract CPAcheckeris a versatile framework for software verification, rooted in the established concept ofconfigurable program analysis. Compared to the last published system description at SV-COMP 2015, theCPAcheckersubmission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses inCPAcheckerand cover the full spectrum of the diverse program characteristics and specifications in the competition, we usestrategy selectionto predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses usingk-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms inCPAcheckerenables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories.CPAcheckeralso generates verification witnesses in the new YAML format.