Sascha Böhme, Anthony Fox, Thomas Sewell, and Tjark Weber. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 183-198. Springer, 2011.
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.
The original publication is available at www.springerlink.com.
@inproceedings{boehme11reconstruction,
author = {Sascha B{\"o}hme and Anthony Fox and Thomas Sewell and Tjark Weber},
title = {Reconstruction of {Z3}'s Bit-Vector Proofs in {HOL4} and {Isabelle/HOL}},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
booktitle = {Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December~7-9, 2011. Proceedings},
volume = {7086},
series = {Lecture Notes in Computer Science},
pages = {183--198},
publisher = {Springer},
year = {2011},
url = {http://dx.doi.org/10.1007/978-3-642-25379-9_15}
}