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.

翻译：我们提出iSMC——首个具备交互式认证能力的自认证模型检验器，该认证范式基于交互式证明系统理论。iSMC是一种基于BDD的符号模型检验器，针对含正义约束的树形时序逻辑（CTL）的任意属性进行验证。在解决模型检验问题实例后，iSMC执行认证程序，能以用户指定的高概率保证答案的正确性。该工具基于Couillard等人在CAV 2023上提出的交互式认证QBF求解器技术，我们对其进行了扩展、优化与重构，使其适配CTL模型检验的需求。