arxiv: 2605.03705 · v1 · submitted 2026-05-05 · 💻 cs.LO

Recognition: unknown

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

Philipp Czerner , Javier Esparza , Konrad Winslow

Authors on Pith no claims yet

Pith reviewed 2026-05-07 13:12 UTC · model grok-4.3

classification 💻 cs.LO

keywords model checkinginteractive certificationBDDCTLsymbolic verificationself-certifyingjustice requirements

0 comments

The pith

iSMC is the first self-certifying model checker with interactive certification for arbitrary CTL properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents iSMC as a BDD-based symbolic model checker for Computation Tree Logic properties that include justice requirements. After solving whether a property holds in a model, iSMC runs an interactive certification procedure drawn from proof systems. This procedure guarantees correctness with a high probability chosen by the user. The system adapts and extends prior interactive certification technology developed for QBF solvers to fit the needs of CTL model checking with BDD data structures. A reader would care because model checking supports safety-critical designs, and self-certification reduces the need to fully trust the checker implementation.

Core claim

iSMC performs BDD-based symbolic model checking for arbitrary CTL properties with justice requirements and then conducts an interactive certification procedure. The procedure is obtained by extending, improving, and re-implementing the interactive certification technology from a prior QBF solver, adapting it to the algorithms and data structures of CTL model checking to deliver a user-chosen high-probability guarantee that the answer is correct.

What carries the argument

Interactive certification procedure adapted from QBF solvers to BDD representations of CTL fixed-point computations and justice constraints.

Load-bearing premise

The interactive certification procedure, when adapted from QBF to the specific BDD algorithms and data structures of CTL model checking, still delivers the claimed high-probability soundness guarantee.

What would settle it

A CTL model-checking instance on which iSMC reports an incorrect answer yet the certification procedure still succeeds with probability above the user-chosen threshold.

Figures

Figures reproduced from arXiv: 2605.03705 by Javier Esparza, Konrad Winslow, Philipp Czerner.

**Figure 1.** Figure 1: At the top, symbolic checking algorithm for the formula EFp (on the left), and one of its possible execution traces (on the right). At the bottom, circuit for this execution. Blue nodes correspond to basic gates, white nodes to “macros”. generalization of the boolean circuits with partial evaluation used in [11] defined below, and a set of equivalence claims. In a nutshell, every instruction of the trace i… view at source ↗

**Figure 2.** Figure 2: Comparison of Apply(v1, v2, ⊛) and our new algorithm ApplyEBDD(v1, v2, ⊛). 5.1 Implementation of Prover by Couillard et al. [11] At first sight, the computations performed by Solver and Prover on an instance of the model-checking problem seem to be unrelated: Solver computes BDDs for the (boolean functions of) the gates of a circuit φ, while Prover computes polynomials for the gates of conv(φ). More precis… view at source ↗

**Figure 3.** Figure 3: eBDDs for Jψ1 ∨ ψ2K, δx1 Jψ1 ∨ ψ2K, and δx2 δx1 Jψ1 ∨ ψ2K, where ψ1 = x1 and ψ2 = x1 ∧ x2, and BDD obtained after simplifying the latter. Solver of [11] just runs ComputeEBDD(v1, v2, ⊛) instead of Apply(v1, v2, ⊛). Appendix D describes the algorithm in detail. The data structure is called extended BDDs (eBDDs). Formally, an eBDD node e is either 0, 1, a node hx, e0, e1i, where x ∈ X and e0, e1 are eBDD no… view at source ↗

**Figure 4.** Figure 4: New computation of immutable eBDDs using links for versioning. We present a new algorithm ApplyEBDD, shown on the right of view at source ↗

**Figure 5.** Figure 5: Top: Solving time (left) and memory consumption (right) of solving instances using iSMC vs. NuSMV. Bottom: iSMC’s Solver vs. iSMC’s Prover computation time. length of the execution trace, while Prover’s time is linear on the time it takes to execute it. Generally, execution traces for larger benchmarks manipulate larger BDDs, which improves the speedup of Verifier w.r.t. Prover; however, some have long tra… view at source ↗

**Figure 6.** Figure 6: Top: Computation time of iSMC’s Prover vs. Verifier. Bottom: iSMC using our improvements vs. blic. checker not only for full CLT, but for the full modal µ-calculus. It can also be used to certify a CTL model-checker that computes predecessors by iterative squaring of the transition relation. The execution sequence of this algorithm always has polynomial length in the size of the model-checking instance, an… view at source ↗

read the original abstract

We present iSMC, the first self-certifying model checker with interactive certification, a certification paradigm based on the theory of interactive proof systems. iSMC is a symbolic BDD-based model checker for arbitrary properties of Computation Tree Logic (CTL) with justice requirements. After solving an instance of the model-checking problem, iSMC conducts a certification procedure that guarantees with high probability (chosen by the user) that the answer is correct. iSMC is based on the technology of the QBF-solver with interactive certification presented by Couillard et al. at CAV 2023. We extend, improve on, and re-implement this technology, adapting it to the needs of CTL model checking.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

iSMC extends the 2023 QBF interactive certification to a BDD-based CTL model checker with justice constraints, which is a practical engineering step but requires explicit validation that the probabilistic guarantee survives the adaptation.

read the letter

The main point is that this paper takes the interactive certification protocol from Couillard et al.'s CAV 2023 QBF solver and re-implements it inside a symbolic BDD model checker for full CTL with justice. That combination is new. They adapt the certification layer to the fixed-point computations for operators like EU and EG, plus the handling of justice requirements, and claim the result gives a user-chosen high-probability guarantee that the model-checking answer is correct. The engineering looks competent because it builds directly on existing BDD infrastructure instead of starting over. If the adaptation is clean, this supplies a usable certification layer for an established verification technique without changing the core algorithms much. The soft spot is exactly the one the stress test flags: whether the original error bound carries over unchanged. BDD variable ordering, the iterative nature of the fixed points, and the specific encoding of justice can create data structures and computation paths that did not exist in the QBF setting. The paper needs to show, either by argument or by bounding any new error sources, that no additional failure modes appear and that the probability remains as advertised. If that step is only sketched or assumed by analogy, the central claim rests on weaker ground than the abstract suggests. This work is for people in the model-checking and certified-verification community who care about making existing tools more trustworthy. A reader already familiar with BDD-based checkers and the 2023 QBF paper will get the most out of the adaptation details. It deserves a serious referee because the idea is concrete, the extension is non-trivial, and the potential impact on safety-critical tool trust is real, even if the soundness argument needs tightening.

Referee Report

1 major / 2 minor

Summary. The manuscript presents iSMC, a BDD-based symbolic model checker for arbitrary CTL properties that include justice requirements. After solving a model-checking instance, iSMC runs an interactive certification procedure adapted from the QBF solver of Couillard et al. (CAV 2023). The procedure is claimed to guarantee correctness with a user-chosen high probability. The work asserts that iSMC is the first self-certifying model checker with interactive certification for CTL and that the prior QBF technology has been extended, improved, and re-implemented to handle BDD representations and CTL fixed-point computations.

Significance. If the adaptation of the interactive certification protocol is shown to preserve the original high-probability soundness guarantee when applied to BDD encodings of CTL operators and justice constraints, the result would be a useful step toward practical self-certifying symbolic model checkers. The explicit credit to the CAV 2023 QBF work and the focus on re-implementation for CTL fixed points and fairness are positive; such tools could increase confidence in verification results for systems with fairness assumptions.

major comments (1)

[Certification procedure (Section 4)] The central claim that the interactive certification provides a user-chosen high-probability guarantee of correctness for CTL model checking rests on the adaptation of Couillard et al.'s QBF protocol to BDD data structures and CTL algorithms. No explicit argument is given showing that the original error bound carries over to the fixed-point computations for operators such as EU and EG, or to the encoding of justice requirements, without introducing new failure modes (e.g., from variable ordering or iteration). This is load-bearing for the soundness claim.

minor comments (2)

The abstract and introduction could more explicitly list the concrete improvements made to the CAV 2023 technology beyond re-implementation for BDD and CTL.
[Preliminaries (Section 2)] Notation for justice constraints and their encoding in the BDD representation should be introduced with a short example in the preliminaries for readers outside the immediate subfield.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. We appreciate the acknowledgment of the work's potential and the explicit credit to the CAV 2023 QBF foundation. We address the major comment below.

read point-by-point responses

Referee: The central claim that the interactive certification provides a user-chosen high-probability guarantee of correctness for CTL model checking rests on the adaptation of Couillard et al.'s QBF protocol to BDD data structures and CTL algorithms. No explicit argument is given showing that the original error bound carries over to the fixed-point computations for operators such as EU and EG, or to the encoding of justice requirements, without introducing new failure modes (e.g., from variable ordering or iteration). This is load-bearing for the soundness claim.

Authors: We agree that an explicit argument for preservation of the error bound is necessary to fully support the central soundness claim. The interactive certification in iSMC applies the protocol from Couillard et al. to the final BDDs produced by the CTL algorithms rather than to the intermediate fixed-point steps. Because the protocol verifies the correctness of the claimed BDD (as a compact representation of the set of states satisfying the property) through random queries on its structure, and because all CTL operators (including EU and EG) are computed via a finite sequence of standard, deterministic BDD operations with a fixed variable ordering chosen upfront, the original probabilistic guarantee carries over directly. Justice requirements are encoded as additional conjunctive BDD constraints that are part of the same final certificate and are therefore covered by the same verification queries. No new failure modes arise from iteration counts or ordering, as the protocol does not depend on the computation history. In the revised manuscript we will add a dedicated subsection to Section 4 containing a formal argument and proof sketch establishing this preservation. revision: yes

Circularity Check

0 steps flagged

No circularity: central claim extends independently published external certification technology

full rationale

The paper's derivation chain consists of adapting and re-implementing the interactive certification procedure from the externally cited Couillard et al. CAV 2023 QBF-solver work to BDD-based CTL model checking with justice constraints. The abstract explicitly positions iSMC as 'based on the technology of the QBF-solver with interactive certification presented by Couillard et al. at CAV 2023' and states that the authors 'extend, improve on, and re-implement this technology'. No self-citations appear in the load-bearing steps, no parameters are fitted and then renamed as predictions, and no uniqueness theorems or ansatzes are smuggled via author-overlapping citations. The probabilistic guarantee is imported from the prior independent publication rather than derived from the present paper's own inputs or definitions. The adaptation itself is presented as an engineering extension whose soundness transfer is asserted but not reduced to a self-referential equation or fit. This satisfies the criteria for a self-contained derivation against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on the established theory of interactive proof systems and the correctness of the prior QBF certification procedure; no new free parameters or invented entities are introduced in the abstract.

axioms (2)

domain assumption Interactive proof systems provide probabilistic soundness guarantees for the certification procedure
Invoked when the abstract states that the certification guarantees correctness with high probability chosen by the user.
domain assumption The QBF interactive certification technology from Couillard et al. (CAV 2023) can be correctly extended and re-implemented for CTL model checking
Central to the adaptation claim in the abstract.

pith-pipeline@v0.9.0 · 5413 in / 1379 out tokens · 43967 ms · 2026-05-07T13:12:26.785238+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

48 extracted references · 1 canonical work pages

[1]

Computational Complexity — A Modern Approach

Sanjeev Arora and Boaz Barak. Computational Complexity — A Modern Approach . Cambridge University Press, 2009

2009
[2]

Armin Biere, Marc Herbstritt, Daniel Le Berre, Siert Wieringa, and Aina Niemetz. Aiger. https://fmv.jku.at/aiger/, 2025

2025
[3]

Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers , C35(8):677–691, 1986

1986
[4]

Randal E. Bryant. Binary decision diagrams. In Handbook of Model Checking , pages 191–217. Springer International Publishing, 2018

2018
[5]

Burch, Edmund M

Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, and David D. Dill. Symbolic model checking for sequential circuit veriﬁcation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems , 13(4):401–424, 1994

1994
[6]

The nuxmv symbolic model checker

Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessan- dro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuxmv symbolic model checker. In CA V, volume 8559 of Lecture Notes in Computer Science , pages 334–342. Springer, 2014. 20 P. Czerner, J. Esparza, K. Winslow

2014
[7]

BDD-based symbolic model checking

Sagar Chaki and Arie Gurﬁnkel. BDD-based symbolic model checking. In Handbook of Model Checking , pages 219–245. Springer International Publishing, 2018

2018
[8]

Nusmv: a new symbolic model checker

Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. Nusmv: a new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT) , 2(4):410–425, 2000

2000
[9]

Clarke, Thomas A

Edmund M. Clarke, Thomas A. Henzinger, and Helmut Veith. Introduction to model checking. In Handbook of Model Checking, pages 1–26. Springer International Publishing, 2018

2018
[10]

Certiﬁcates for parameterized model checking

Sylvain Conchon, Alain Mebsout, and Fatiha Zaïdi. Certiﬁcates for parameterized model checking. In FM, volume 9109 of Lecture Notes in Computer Science , pages 126–142. Springer, 2015

2015
[11]

Making IP=PSPACE practical: Eﬃcient interactive protocols for BDD algorithms

Eszter Couillard, Philipp Czerner, Javier Esparza, and Rupak Majumdar. Making IP=PSPACE practical: Eﬃcient interactive protocols for BDD algorithms. In CA V (3), volume 13966 of Lecture Notes in Computer Science , pages 437–458. Springer, 2023

2023
[12]

A resolution-based inter- active proof system for UNSAT

Philipp Czerner, Javier Esparza, and Valentin Krasotin. A resolution-based inter- active proof system for UNSAT. In FoSSaCS (2) , volume 14575 of Lecture Notes in Computer Science , pages 116–136. Springer, 2024

2024
[13]

Sometimes

E. Allen Emerson and Joseph Y. Halpern. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. Journal of the ACM , 33(1):151–178, 1986

1986
[14]

A fully veriﬁed executable LTL model checker

Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully veriﬁed executable LTL model checker. In CA V, volume 8044 of Lecture Notes in Computer Science , pages 463–478. Springer, 2013

2013
[15]

Certifying phase ab- straction

Nils Froleyks, Emily Yu, Armin Biere, and Keijo Heljanko. Certifying phase ab- straction. In IJCAR (1) , volume 14739 of Lecture Notes in Computer Science , pages 284–303. Springer, 2024

2024
[16]

The knowledge complexity of interactive proof-systems (extended abstract)

Shaﬁ Goldwasser, Silvio Micali, and Charles Rackoﬀ. The knowledge complexity of interactive proof-systems (extended abstract). In STOC, pages 291–304. ACM, 1985

1985
[17]

Certifying proofs for sat- based model checking

Alberto Griggio, Marco Roveri, and Stefano Tonetta. Certifying proofs for sat- based model checking. Formal Methods Syst. Des. , 57(2):178–210, 2021

2021
[18]

Extended resolution proofs for sym- bolic sat solving with quantiﬁcation

Toni Jussila, Carsten Sinz, and Armin Biere. Extended resolution proofs for sym- bolic sat solving with quantiﬁcation. In Theory and Applications of Satisﬁability Testing - SAT 2006 , pages 54–60. Springer Berlin Heidelberg, 2006

2006
[19]

Meel, and Ning Luo

Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, and Ning Luo. Towards prac- tical zero-knowledge proof for PSPACE. 2025. arXiv:2511.15071 [cs.CR]

work page arXiv 2025
[20]

Increasing conﬁdence in liveness model checking results with proofs

Tuomas Kuismin and Keijo Heljanko. Increasing conﬁdence in liveness model checking results with proofs. In Haifa Veriﬁcation Conference , volume 8244 of Lecture Notes in Computer Science , pages 32–43. Springer, 2013

2013
[21]

Algebraic meth- ods for interactive proof systems

Carsten Lund, Lance Fortnow, Howard Karloﬀ, and Noam Nisan. Algebraic meth- ods for interactive proof systems. Journal of the ACM , 39(4):859–868, 1992-10

1992
[22]

Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang

Ning Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang. Proving unsat in zero knowledge. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security , CCS 22, pages 2203–2217. ACM, 2022-11

2022
[23]

Cacbdd: A BDD package with dynamic cache management

Guanfeng Lv, Kaile Su, and Yanyan Xu. Cacbdd: A BDD package with dynamic cache management. In CA V, volume 8044 of Lecture Notes in Computer Science , pages 229–234. Springer, 2013. A BDD-based Symbolic Model Checker with Interactive Certiﬁcation 21

2013
[24]

McMillan

Kenneth L. McMillan. Symbolic model checking . Kluwer, 1993

1993
[25]

Proof certiﬁcates for smt-based model checkers for inﬁnite-state systems

Alain Mebsout and Cesare Tinelli. Proof certiﬁcates for smt-based model checkers for inﬁnite-state systems. In FMCAD, pages 117–124. IEEE, 2016

2016
[26]

Namjoshi

Kedar S. Namjoshi. Certifying model checkers. In Computer Aided Veriﬁcation , pages 2–13. Springer Berlin Heidelberg, 2001

2001
[27]

Temporal logic and fair discrete systems

Nir Piterman and Amir Pnueli. Temporal logic and fair discrete systems. In Handbook of Model Checking , pages 27–73. Springer International Publishing, 2018

2018
[28]

HWMCC’25 benchmarks and results, 2025

Mathias Preiner, Nils Froleyks, and Armin Biere. HWMCC’25 benchmarks and results, 2025

2025
[29]

IP = PSPACE

Adi Shamir. IP = PSPACE. Journal of the ACM , 39(4):869–877, 1992-10

1992
[30]

CUDD: CU Decision Diagram Package Release 3.0.0 , 2015-12-31

Fabio Somenzi. CUDD: CU Decision Diagram Package Release 3.0.0 , 2015-12-31

2015
[31]

A veriﬁed model checker for the modal µ-calculus in coq

Christoph Sprenger. A veriﬁed model checker for the modal µ-calculus in coq. In TACAS, volume 1384 of Lecture Notes in Computer Science , pages 167–183. Springer, 1998

1998
[32]

Coqcryptoline: A veriﬁed model checker with certiﬁed results

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, and Bo- Yin Yang. Coqcryptoline: A veriﬁed model checker with certiﬁed results. In CA V (2), volume 13965 of Lecture Notes in Computer Science , pages 227–240. Springer, 2023

2023
[33]

Blumberg

Michael Walﬁsh and Andrew J. Blumberg. Verifying computations without reexe- cuting them. Communications of the ACM , 58(2):74–84, 2015

2015
[34]

Munta: A veriﬁed model checker for timed automata

Simon Wimmer. Munta: A veriﬁed model checker for timed automata. In FORMATS, volume 11750 of Lecture Notes in Computer Science , pages 236–243. Springer, 2019

2019
[35]

Bryant, David R

Bwolen Yang, Randal E. Bryant, David R. OHallaron, Armin Biere, Olivier Coud- ert, Geert Janssen, Rajeev K. Ranjan, and Fabio Somenzi. A performance study of bdd-based model checking. In Formal Methods in Computer-Aided Design , pages 255–289. Springer Berlin Heidelberg, 1998

1998
[36]

Progress in certifying hardware model checking results

Emily Yu, Armin Biere, and Keijo Heljanko. Progress in certifying hardware model checking results. In CA V (2), volume 12760 of Lecture Notes in Computer Science , pages 363–386. Springer, 2021

2021
[37]

Stratiﬁed certiﬁcation for k-induction

Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko. Stratiﬁed certiﬁcation for k-induction. In FMCAD, pages 59–64. IEEE, 2022

2022
[38]

x belongs to L

Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko. Towards compositional hardware model checking certiﬁcation. In FMCAD, pages 1–11. IEEE, 2023. 22 P. Czerner, J. Esparza, K. Winslow A Preliminaries A.1 Binary Decision Diagrams (BDDs) We recall basic notions on reduced ordered binary decision diagrams [ 3,4], called in this paper BDDs for short. BD...

2023
[39]

Figure D.1 illustrates an example of how eBDDs are used to encode polynomials of an underlying circuit

introduced the data structure of extended BDDs . Figure D.1 illustrates an example of how eBDDs are used to encode polynomials of an underlying circuit. On the left is the GBC φ = δ1δ2ψ with ψ = v1_ (v1^ v2) (conv would also add degree reductions to v1^ v2). To the right of the GBC are three eBDDs for JψK, Jδ2ψK, and Jδ1δ2ψK. The polynomial equal to both ...
[40]

[ [r] ] = [ [f ] ]⊛ [ [g] ]
[41]

If w is a binary operation node, all its children are ﬁnal BDD nodes
[42]

lk(w) =hvk, l′, r′i is either a standard eBDD or ﬁnal BDD node that fulﬁlls vk = var(w) and [ [lk(w)] ] =vk π[vk:=1][ [w] ] + (1 vk) π[vk:=0][ [w] ]
[43]

We call BDDs ﬁnal if they do not contain any binary operation nodes and thus represent standard BDDs

lk(lk(w)) = u is a ﬁnal BDD. We call BDDs ﬁnal if they do not contain any binary operation nodes and thus represent standard BDDs. [ [u] ] =δ1 δn[ [r] ] for n being the number of variables in [ [w] ]
[44]

Next, we prove using induction on ApplyEBDD’s recursive call graph that it maintains eBDD invariants

w is a ﬁnal BDD iﬀ lk(w) = w. Next, we prove using induction on ApplyEBDD’s recursive call graph that it maintains eBDD invariants. Lemma D.1 (ApplyEBDD(f, g, ⊛) [correctness]). Given ﬁnal eBDD arguments f, g that adhere to the invariants (Def. D.1), the result r = ApplyEBDD(u, w, ⊛) also adheres to said invariants. Proof. We proceed by f-induction on Com...
[45]

At the ﬁrst invocation of TraceCertRev(φ,C), Veriﬁer creates a random assignment σ for all n variables
[46]

Each time TraceCert samples a random value for a variable vk $ Fp, TraceCertRev instead uses the random assignment vk σ(vk) computed at the beginning
[47]

Checking this claim allows Veriﬁer to propagate claims to φ’s parents in the next invocation: Veriﬁer replaces ψ by a new GBC node type εψ k after running TraceCertRev

Veriﬁer adds the claim ΠσJψK = k toC for each node ψ2 φ. Checking this claim allows Veriﬁer to propagate claims to φ’s parents in the next invocation: Veriﬁer replaces ψ by a new GBC node type εψ k after running TraceCertRev. Note that this node type does not have any children, so unreachable nodes can be garbage collected
[48]

σ′6= σ or k6= k′

In subsequent invocations, when checking a claim Πσ′ [ [εψ k ] ] =k′ (correspond- ing to a previously removed node), Veriﬁer rejects iﬀ. σ′6= σ or k6= k′. The main text explains how, if a dishonest Prover can ‘remember’ old chal- lenges, then TraceCertRev would no longer be sound. However, under the rea- sonable assumption that Prover does not store previ...