Conference proceeding
Proof certificates for SMT-based model checkers for infinite-state systems
2016 Formal Methods in Computer-Aided Design (FMCAD), pp.117-124
10/2016
DOI: 10.1109/FMCAD.2016.7886669
Abstract
We present a dual technique for generating and verifying proof certificates in SMT-based model checkers, focusing on proofs of invariant properties. Certificates for two major model checking algorithms are extracted as k-inductive invariants, minimized and then reduced to a formal proof term with the help of an independent proof-producing SMT solver. SMT-based model checkers typically translate input problems into an internal first-order logic representation. In our approach, the correctness of translation from the model checker's input to the internal representation is verified in a lightweight manner by proving the observational equivalence between the results of two independent translations. This second proof is done by the model checker itself and generates in turn its own proof certificate. Our experimental evaluation show that, at the price of minimal instrumentation in the model checker, the approach allows one to efficiently generate and verify proof certificates for non-trivial transition systems and invariance queries.
Details
- Title: Subtitle
- Proof certificates for SMT-based model checkers for infinite-state systems
- Creators
- Alain Mebsout - Univ. of Iowa, Iowa City, IA, USACesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2016 Formal Methods in Computer-Aided Design (FMCAD), pp.117-124
- DOI
- 10.1109/FMCAD.2016.7886669
- Publisher
- FMCAD Inc
- Language
- English
- Date published
- 10/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984259461102771
Metrics
15 Record Views