Paper Info
Title
Reconstruction of z3's bit-vector proofs in HOL4 and Isabelle/HOL
Abstract
The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of unsatisfiability proofs for bit-vector theories in the theorem provers HOL4 and Isabelle/HOL. Our work shows that LCF-style proof reconstruction for the theory of fixed-size bit-vectors, although difficult because Z3's proofs provide limited detail, is often possible. We thereby obtain high correctness assurances for Z3's results, and increase the degree of proof automation for bit-vector problems in HOL4 and Isabelle/HOL.
Year
DOI
Venue
2011
10.1007/978-3-642-25379-9_15
CPP
Keywords
Field
DocType
bit-vector problem,satisfiability modulo theories,lcf-style proof reconstruction,solver z3,high correctness assurance,bit-vector proof,unsatisfiability proof,proof automation,bit-vector theory,fixed-size bit-vectors,independent reconstruction
Theorem provers,HOL,Computer science,Correctness,Algorithm,Automation,Mathematical proof,Solver,Bit array,Satisfiability modulo theories
Conference
Citations 
PageRank 
References 
15
0.64
21
Authors
4
Name
Order
Citations
PageRank
Sascha Böhme121612.94
Anthony C. J. Fox217510.70
Thomas Sewell391437.60
Tjark Weber421519.33