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

TL;DR

iSMC is a novel self-certifying symbolic model checker for CTL properties, utilizing interactive proof systems to guarantee correctness with high probability, based on advanced QBF-solving technology.

Contribution

The paper introduces iSMC, the first self-certifying CTL model checker with interactive certification, extending and adapting QBF-based certification technology.

Findings

iSMC guarantees correctness with high probability after model checking.

It is the first to combine symbolic BDD-based model checking with interactive certification.

The approach extends previous QBF-solver technology to CTL model checking.

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.