Showing 2026Show all
2 papers · 1 filter
cs.LO2026
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…
cs.LO2026
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…