CPV: A Circuit-Based Program Verifier

Software verification is challenging. Numerous intermediate representations have been proposed to capture diverse software features and facilitate the development of program verifiers. Among various encodings of a state-transition system, sequential circuits, consisting of memory elements to represent states and combinational logic to capture state transitions, are commonly used in the hardware-verification domain, and abundant techniques have been invented for hardware model checking. Using sequential circuits as its intermediate representation, our tool CPV aims to answer the following question: Are sequential circuits feasible as an alternative foundation to build software verifiers? While previous studies on translating and cross-applying verification techniques for hardware and software exist [1,2,3,4], to our knowledge, no participants in SV-COMP had used sequential circuits as their intermediate representations. This competition report outlines the software architecture and verification approach of CPV and discusses its results against other mature program analyzers in SV-COMP 2024 [5].

Software architecture of CPV

Full size image

The software architecture of CPV is depicted in Fig. 1. Its verification workflow is divided into two stages: (1) In the frontend (the upper half of Fig. 1), an input C program with a reachability-safety property is first instrumented to allow for witness translation (details in Sect. 3) and then translated into a word-level Btor2  [7] circuit by Kratos2  [6]. The Btor2 language [7] is used in the Hardware Model Checking Competitions [14, 15], and many powerful hardware model checkers support this format. A bit-level Aiger  [9] circuit is also generated by the tool Btor2Aiger  [8]; (2) In the backend (the lower half of Fig. 1), CPV invokes hardware model checkers AVR  [10] and ABC  [11] to verify the translated circuits. Btor2 verification witnesses produced for the circuits are translated to software witnesses in the GraphML format [13] for the original program. CPV configures and executes the backend model checkers (either solely or as portfolios) via CoVeriTeam  [12], a library for cooperative verification [16]. Thanks to the versatility of CoVeriTeam, it is convenient to choose the verification algorithms used by AVR and ABC, and the pool of the backend verifiers in CPV can be expanded with little effort.

The approach of CPV is to translate a program into a circuit and applies hardware model checking to the translated verification task. To generate software-verification witnesses, CPV instruments an input program before translating it to a circuit, such that the information contained in a witness for the translated circuit can be mapped back to the original program.

Program-to-Circuit Translation. CPV utilizes Kratos2  [6] as its frontend to translate a verification task of a C program into a word-level sequential circuit in the Btor2 format [7]. Kratos2 applies large-block encoding [17] and introduces a symbolic program counter to fold the summarized program into a state-transition system. Executing a maximal loop-free block of the program is a one-step transition in the system. A call to an external function that models nondeterministic input values to the program, e.g., the functions \(\texttt {{\_}{\_}VERIFIER\_nondet\_X()}\) in SV-COMP, is represented as an external input to the state-transition system. We configure Kratos2 to export the system as a sequential circuit in the Btor2 format because Btor2 is the prevailing format for hardware model checking. In order to leverage bit-level hardware model checkers, CPV additionally invokes Btor2Aiger  [8] to translate the word-level Btor2 circuit into the Aiger format [9]. Currently, CPV supports the property of reachability safety. Violation to the reachability-safety property of the input program is captured by a circuit output asserting the equivalence between the symbolic program counter and the error location.

Hardware Model Checking. CPV employs AVR  [10] and ABC  [11], two state-of-the-art hardware model checkers for word-level Btor2 and bit-level Aiger circuits, respectively, to analyze the translated circuits. A hardware model checker decides whether the translated circuit has a computation trace to assert its circuit output, which indicates the error location in the original program is reachable. In this case, the verification verdict is false, and the original program is unsafe. If there is no trace to assert the circuit output, the verdict is true, and the original program is safe.

To achieve synergy, we combine the strengths of various hardware-verification algorithms, including property-directed reachability (PDR) [18, 19], interpolation-based model checking (IMC) [20], \(k\)-induction (KI) [21], and bounded model checking (BMC) [22]. For the tasks that can be translated into Aiger circuits,^{Footnote 1} a sequential portfolio of AVR-KI, AVR-PDR, ABC-IMC, ABC-PDR, and AVR-BMC is applied. A pre-determined time limit is imposed on each component in the portfolio by CoVeriTeam. AVR is executed first in the portfolio because it can produce a Btor2 witness [7] for the translated circuit if a property violation was found, whereas ABC does not export witnesses in a standardized format. CPV can then translate a Btor2 witness back to a software violation witness. Currently, CPV outputs a dummy violation witness if a bug is reported by ABC. Since both the Btor2 and Aiger languages do not define a format for correctness witnesses, CPV also outputs a dummy correctness witness in this case. For the remaining tasks that cannot be translated into Aiger circuits, CPV uses a sequential portfolio of AVR ’s KI, PDR, and BMC.

Program Instrumentation for Witness Translation. To map the information in a Btor2 witness back to the original program, CPV instruments the input program prior to the program-to-circuit translation. A Btor2 violation witness encodes a computation trace that asserts the output of the translated circuit. The trace consists of a sequence of values given to the circuit’s external inputs, each corresponding to a call to a function \(\texttt {{\_}{\_}VERIFIER\_nondet\_X()}\) in the program. To assume these values at the control-flow locations where they are relevant for triggering the property violation, CPV ’s instrumentor assigns a fresh counter to each of these calls. A counter is incremented after each call, so its value can be inferred from the Btor2 witness. An input value is relevant if accompanied by a change in its counter. The witness translator of CPV traverses the Btor2 witness, extracts the relevant input values by tracking the changes in the counters, and exports the software violation witness in the GraphML format [13].

CPV participated in the category ReachSafety of SV-COMP 2024 [5]. As a first-year participant, it surprisingly outperformed several mature software verifiers in terms of the number of correctly solved tasks. CPV is especially effective in the subcategory ReachSafety-Hardware and ReachSafety-ECA, solving the second and third most tasks among all participants, respectively. Its impressive results manifest the feasibility of using sequential circuits as an alternative intermediate representation to construct program verifiers.

The overall results of CPV is summarized in Table 1. Among the 11 222 verification tasks in the category ReachSafety, 8 439 were successfully translated to Btor2 circuits by Kratos2, and 7 773 could be further translated to Aiger circuits by Btor2Aiger. In total, CPV produced 4 952 correct and confirmed results. The \(k\)-inductionimplementation in AVR contributed the most correctly solved and confirmed tasks, followed by PDR of AVR and IMC of ABC.^{Footnote 2}

We will improve CPV in the following directions: First, we will generate non-trivial software correctness witnesses through extracting and translating the fixed points computed by hardware model checkers. We aim to enhance the witness-confirmation rate of CPV, currently about \({90}\,{\%}\), to the level of other mature participants (more than \({95}\,{\%}\)). Second, we will investigate the 27 false alarms in the subcategory ReachSafety-Hardness.

We submitted CPV at version 0.4 [23] to SV-COMP 2024 [5]. A Linux-based operating system is required to execute the tool, as the used library CoVeriTeam  [12] relies on Linux-specific features, such as control groups, name spaces, and overlay file systems. Additional Python package requirement and the instructions to set up the execution environment can be found in the README file of the submitted tool archive.