A framework for proof certificates in finite state exploration
Quentin Heath (Inria & LIX), Dale Miller (Inria & LIX)

TL;DR
This paper introduces a flexible framework for generating and verifying proof certificates in finite state exploration, enhancing trustworthiness of model checking results across various properties.
Contribution
It presents a formal, sound framework for proof certificates in model checking, applicable to multiple properties like reachability and bisimulation, with an implemented reference checker.
Findings
Framework guarantees soundness independently of clerk and expert correctness.
Proof certificates successfully verified for reachability, non-reachability, and bisimulation.
Implemented a reference proof checker for the framework.
Abstract
Model checkers use automated state exploration in order to prove various properties such as reachability, non-reachability, and bisimulation over state transition systems. While model checkers have proved valuable for locating errors in computer models and specifications, they can also be used to prove properties that might be consumed by other computational logic systems, such as theorem provers. In such a situation, a prover must be able to trust that the model checker is correct. Instead of attempting to prove the correctness of a model checker, we ask that it outputs its "proof evidence" as a formally defined document--a proof certificate--and that this document is checked by a trusted proof checker. We describe a framework for defining and checking proof certificates for a range of model checking problems. The core of this framework is a (focused) proof system that is augmented…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
