3 citations · 6 across the 8 of their papers we have counts for
4 papers · 1 filter
iSMC: A BDD-based Symbolic Model Checker with Interactive Certification
Philipp Czerner, Javier Esparza, Konrad Winslow
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 symbol…
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
Michael Blondin, Michaël Cadilhac, Xin-Yi Cui +3
Ordered binary decision diagrams (OBDDs) are a fundamental data structure for the manipulation of Boolean functions, with strong applications to finite-state symbolic model checkin…
A Resolution-Based Interactive Proof System for UNSAT
Philipp Czerner, Javier Esparza, Valentin Krasotin +1
Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless NP=coNP), and at recent SAT competitions…
Making Practical: Efficient Interactive Protocols for BDD Algorithms
Eszter Couillard, Philipp Czerner, Javier Esparza +1
We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasonin…