Technical Summary: iSMC – A BDD-based Symbolic Model Checker with Interactive Certification

1. Problem Statement

Model checking is a fundamental technique for verifying the correctness of hardware and software systems. However, ensuring the reliability of the model checker itself is a critical challenge. Traditional certification paradigms rely on non-interactive protocols: a prover (the model checker) generates a certificate (e.g., a satisfying assignment or a resolution proof), and a verifier checks it independently.

The paper identifies a fundamental theoretical limitation in this approach: for many problems, including general CTL model checking, certificates can have worst-case exponential length in the size of the instance. Consequently, the verifier requires exponential time to check them, rendering the certification process impractical for large systems unless $NP = coNP$.

The authors propose interactive certification, a paradigm based on interactive proof systems (IP), where a prover and verifier engage in a multi-round protocol. The verifier adaptively asks questions, allowing it to detect errors with high probability in polynomial time, even if the underlying computation is complex. While interactive proofs for PSPACE problems (like CTL model checking) are theoretically established (Shamir's $IP=PSPACE$), making them practical for symbolic model checking using Binary Decision Diagrams (BDDs) has remained an open challenge.

2. Methodology

The paper presents iSMC, the first self-certifying model checker that implements interactive certification for CTL model checking with justice requirements. The system is built upon three core modules:

2.1 Architecture

• Solver: A symbolic BDD-based model checker that computes the set of reachable states satisfying a CTL specification. It operates on flattened boolean models (SMV format) and uses the clic BDD library.
• Prover: Runs on the same machine as the Solver. It executes the model checking instance and generates an execution trace consisting of the sequence of BDD library calls and assertions made during the computation.
• Verifier: A lightweight module that can run on a client with limited resources. It does not re-execute the model checking algorithm. Instead, it engages in an interactive protocol with the Prover to verify the execution trace.

2.2 The TraceCert Protocol

The core innovation is TraceCert, an interactive proof protocol adapted from the QBF-certification work of Couillard et al. [11].

1. Trace to Circuit: The execution trace is transformed into a Generalized Boolean Circuit (GBC). Each instruction in the trace becomes a gate, and assertions (e.g., "state set $C_1$ is not equivalent to $C_0$") become equivalence claims.
2. Arithmetization: Boolean functions are encoded as multivariate polynomials over a finite field $\mathbb{F}_p$. This allows the verifier to check properties of the computation by evaluating polynomials at random points rather than traversing the entire circuit.
3. Degree Reduction: To ensure the polynomials have low degree (necessary for polynomial-time verification), the protocol introduces degree-reduction gates ($\delta_x$) that reduce exponents to 1 without changing the function's value on boolean inputs.
4. Interactive Rounds: The protocol proceeds in rounds, traversing the circuit. The Prover claims the value of a gate; the Verifier challenges the Prover with random assignments to the gate's inputs. The Prover must provide polynomials consistent with the claim. If the Prover lies, the probability of being caught is bounded by the Schwartz-Zippel lemma.

2.3 Key Technical Improvements over Prior Work

The authors extend the technology from [11] (which focused on QBF) to handle the specific needs of CTL model checking, addressing three major bottlenecks:

1. Efficient Renaming and Equivalence: The original protocol (CPCertify) handled equivalence and renaming gates inefficiently ($O(n^2)$ and $O(n^k)$). TraceCert optimizes these rounds to $O(1)$ and $O(n)$ respectively.
2. Garbage Collection Compatibility: Standard BDD libraries use global computation caches and garbage collection. The previous approach required the Prover to store all intermediate BDDs, preventing garbage collection. The authors introduce TraceCertRev, a bottom-up variant of the protocol that allows the Prover to discard intermediate results (acting as an oracle) without compromising soundness, provided the Prover does not maliciously conspire to remember past challenges.
3. Global Computation Cache: The previous implementation (blic) could not use a global cache because it manipulated extended BDDs (eBDDs) in a way incompatible with caching. The authors introduce a novel immutable eBDD representation using link fields to version nodes, enabling the use of a global unique table and significantly improving performance.

3. Key Contributions

1. iSMC System: The first implementation of a self-certifying model checker with interactive certification for arbitrary CTL properties with justice requirements.
2. TraceCert Protocol: A new interactive proof protocol that efficiently handles variable renaming and equivalence assertions common in model checking traces, reducing the complexity of specific gate rounds.
3. Optimized eBDD Implementation: A new algorithm (ApplyEBDD) and data structure that enables the use of global computation caches and garbage collection, overcoming the inefficiencies of the previous blic library.
4. TraceCertRev: A protocol variant that allows for garbage collection during certification, making the system viable for large-scale model checking where memory is a constraint.

4. Experimental Results

The authors evaluated iSMC on 53 benchmarks from the HWMCC'25 liveness track.

• Solver Performance: Compared to the mature tool NuSMV, iSMC's Solver is on average 5.84 times slower. The authors attribute this primarily to the lack of support for relational products (a BDD optimization) in the current prototype, as certifying them interactively remains an open problem.
• Prover Overhead: The Prover runs in time $O(S)$, where $S$ is the Solver's time. The constant factor is approximately 2.00, meaning the certification overhead is roughly double the solving time.
• Verifier Efficiency: The Verifier is highly efficient. For a 15-minute timeout on the Prover, the Verifier never took more than 3.6 seconds (average speedup of 33.4x over the Prover). The Verifier's runtime scales linearly with the length of the execution trace, not the computation time.
• Impact of Optimizations: The improvements (TraceCert, clic library, global cache) resulted in an average 2.26x speedup in execution time and a 16.12x reduction in memory usage compared to the baseline implementation using CPCertify and blic.

5. Significance and Claims

The paper claims that iSMC represents a significant step toward practical interactive certification for model checking.

• Trust in Untrusted Servers: The system enables a scenario where a client with limited resources can delegate model checking to a powerful but untrusted server. The server (Solver + Prover) performs the heavy computation, while the client (Verifier) certifies the result with high probability in polynomial time.
• Polynomial Verification: Unlike non-interactive certification methods which require exponential time for general CTL properties, iSMC's Verifier runs in polynomial time relative to the number of variables and the trace length.
• Scalability: The authors demonstrate that with their optimizations, the overhead of interactive certification is manageable, and the memory footprint is significantly reduced, making the approach feasible for non-trivial benchmarks.

The authors remain modest, noting that iSMC is a first prototype. They acknowledge that the Solver is currently slower than state-of-the-art tools like NuSMV due to missing optimizations (relational products) and that the current implementation targets CTL, though the underlying framework could theoretically extend to the full modal $\mu$-calculus.