Abstract Whenever automatic software verifiers determine that a program fulfills or violates its specification, they are expected to produce also a witness that justifies the verdict. This allows a third party to independently validate the verdict and the arguments from which it was derived, increasing trust in the results. The current standard exchange format for witnesses in software verification does not support program termination. To fill this gap, we propose an extension of the witness format that is based on transition invariants as a general and effective formalism. We justify this by (a) proving that transition invariants can encode other popular termination arguments, such as ranking functions, and (b) providing three different validation approaches for transition invariants, which together can validate most of the produced witnesses. Our approach based on transition invariants was integrated into version 2.1 of the exchange format for verification witnesses, our experiments show that the new witnesses can be effectively validated and that validation is often more efficient than verification, and the software-verification community has adopted the format already for SV-COMP 2026.

Designing algorithms for complex problems as certifying algorithms is an important approach to ensure correctness of computational results. Instead of producing an output y for an input x, a certifying algorithm produces as output for x not only y but also a witness w. The witness w (also called certificate) can now be used to check that y is indeed the correct output for input x. Witnesses and their validation also exist in the area of automatic software verification, and a large number of tools support verification witnesses. SV-COMP 2025 reports 62 verifiers producing witnesses and 18 tools for witness validation. In 2023, a new version 2.0 of the witness format for software verification was introduced to overcome several problems with the previous format, and this new format is now widely supported. However, there is no format with a clear definition and semantics for witnesses of non-termination. This paper closes this gap by presenting an extension of the witness format 2.0 to support program non-termination. Besides explaining the design of this extension, we describe various approaches to generate and validate non-termination witnesses. We also give an overview of current tool support of the extended format, i.e., the verifiers that can generate non-termination witnesses and the witness validators able to analyze these witnesses. Finally, we present an experimental evaluation showing the performance of these tools on program-termination tasks of SV-COMP 2025.

Abstract Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on basic reachability properties. Instead of implementing algorithms for each possible specification, some verifiers implement known transformations from the given specification to reachability on their internal representations. Unfortunately, those internal transformations are not reusable by others. To improve this situation, we propose TransVer , a tool which offers transformations as modular stand-alone component, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata , inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination , no-overflow , and memory cleanup . We conduct experiments with ten different verifiers. The experiments evaluate the efficiency and effectiveness of our transformations. The results are promising: Our transformations can extend existing verifiers to be effective on specifications for which they have no integrated support, and the efficiency is often similar or better to state-of-the-art verifiers that have integrated support for the considered specifications.

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 Tight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.

Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and highlights its primary use cases in facilitating scalable benchmarking.

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.