iSMC: A BDD-based Symbolic Model Checker with Interactive Certification
Logic in Computer Science
2026-05-06 v1
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.
Keywords
Cite
@article{arxiv.2605.03705,
title = {iSMC: A BDD-based Symbolic Model Checker with Interactive Certification},
author = {Philipp Czerner and Javier Esparza and Konrad Winslow},
journal= {arXiv preprint arXiv:2605.03705},
year = {2026}
}