Proof certificates for SMT-based model checkers for infinite-state systems

FMCAD, pp. 117-124, 2016.

Cited by: 12|Bibtex|Views8|Links
EI

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...More

Code:

Data:

Your rating :
0

 

Tags
Comments