The International Competition on Software Verification (SV-COMP) has been an important driver of progress in the formal verification community, fostering tool development, benchmarking, and reproducibility. As the competition grows in scale and complexity, a reproducibility study is essential to evaluate its robustness across environments, uncover hidden dependencies, and ensure long-term sustainability. This work aims to reaffirm the reliability of SV-COMP’s results, provide insights for similar competitions, and facilitate the adoption of its infrastructure beyond the competition. We reproduced the verification and validation results of active participants, including score and ranking calculations for the verification track. We found several problems prohibiting reusability and reproducibility of some participating tools, but we did not find serious issues with the competition infrastructure itself.

Due to their decentralized and trustless nature, blockchain and distributed ledger technologies are increasingly used in several domains, including critical applications. The behavior of such blockchain-integrated systems is typically driven by smart contracts. However, smart contracts are application-specific software and may contain faults with severe system-level impacts. This is especially true in the case of the extensively used Hyperledger Fabric (HLF) platform, where smart contracts are written in general-purpose languages (Java, among others), and applications can go far beyond handling virtual-currency-like assets. In this work, we present a novel formal-verification-based approach to smart contract verification and a high-level empirical model of the HLF platform. Our Smart Contract in the Loop (SCIL) method uses a model checker (Java Pathfinder) to check whether specific error properties hold for a given smart contract, while a predefined combination of platform-level fault modes is active. We facilitate the checking of HLF smart contracts without modification and enable the propagation or non-propagation of platform faults through the smart contracts to the system failure level.

Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support.

Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2 - Cert to verify safety properties of Btor2 circuits, combining Btor2 -to-C translation, software verifiers, and a new witness validator Btor2 - Val , to answer the above open questions. Btor2 - Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses , we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2 - Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification . In our evaluation, Btor2 - Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier Cbmc on translated programs, it uniquely solved, with confirmed witnesses, 8 % of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.

Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification.Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms.Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms.One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location.We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples.We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.

Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta , a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category.

ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach.

PLCverif is an actively developed project at CERN, enabling the formal verification of Programmable Logic Controller (PLC) programs in critical systems. In this paper, we present our work on improving the formal requirements specification experience in PLCverif through the use of natural language. To this end, we integrate NASA’s FRET, a formal requirement elicitation and authoring tool, into PLCverif. FRET is used to specify formal requirements in structured natural language, which automatically translates into temporal logic formulae. FRET’s output is then directly used by PLCverif for verification purposes. We discuss practical challenges that PLCverif users face when authoring requirements and the FRET features that help alleviate these problems. We present the new requirement formalization workflow and report our experience using it on two critical CERN case studies.

THETA is a model checking framework based on abstraction refinement algorithms. In SV-COMP 2022, we introduce: 1) reasoning at the source-level via a direct translation from C programs; 2) support for concurrent programs with interleaving semantics; 3) mitigation for non-progressing refinement loops; 4) support for SMT-LIB-compliant solvers. We combine all of the aforementioned techniques into a portfolio with dynamic algorithm selection.

With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.

With the improvement of hardware and algorithms, the main challenge of software model checking has shifted from pure algorithmic performance toward supporting a wider set of input programs. Successful toolchains tackle the problem of parsing a wide range of inputs in an efficient way by reusing solutions from existing compiler technologies such as Eclipse CDT or LLVM. Our experience suggests that well-established techniques in compiler technology are not necessarily beneficial to model checkers and sometimes can even hurt their performance. In this paper, we review the tools mature enough to participate in the Software Verification Competition in terms of the employed analysis and frontend techniques. We find that successful tools do exhibit a bias toward certain combinations. We explore the theoretical reasons and suggest an adaptable approach for model checking frameworks. We validate our recommendations by implementing a new frontend for a model checking framework and show that it indeed benefits some of the algorithms.

Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer , supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.