Proof certificates for SMT-based model checkers for infinite-state systems
FMCAD, pp. 117-124, 2016.
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
Full Text (Upload PDF)
PPT (Upload PPT)