Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.03705 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918484775010304 |
|---|---|
| author | Czerner, Philipp Esparza, Javier Winslow, Konrad |
| author_facet | Czerner, Philipp Esparza, Javier Winslow, Konrad |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_03705 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | iSMC: A BDD-based Symbolic Model Checker with Interactive Certification Czerner, Philipp Esparza, Javier Winslow, Konrad Logic in Computer Science 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. |
| title | iSMC: A BDD-based Symbolic Model Checker with Interactive Certification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.03705 |