iSMC: A BDD-based Symbolic Model Checker with Interactive Certification
For users of formal verification tools, iSMC provides a novel way to gain confidence in model checking results through interactive certification, addressing the trust issue in automated verifiers.
iSMC is the first self-certifying model checker that uses interactive proof systems to certify CTL model checking results with high probability chosen by the user.
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.