“Fine-grained SMT Proofs for the Theory of Fixed-width Bit-vectors” by Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, and Morgan Deters. In Proceedings of the 20^th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '15), (Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, eds.), Nov. 2015, pp. 340-355. Suva, Fiji.
Many high-level verification tools rely on SMT solvers to efficiently discharge complex verification conditions. Some applications require more than just a yes/no answer from the solver. For satisfiable quantifier-free problems, a satisfying assignment is a natural artifact. In the unsatisfiable case, an externally checkable proof can serve as a certificate of correctness and can be mined to gain additional insight into the problem. We present a method of encoding and checking SMT-generated proofs for the quantifier-free theory of fixed-width bitvectors. Proof generation and checking for this theory poses several challenges, especially for proofs based on reductions to propositional logic. Such reductions can result in large resolution subproofs in addition to requiring a proof that the reduction itself is correct. We describe a fine-grained proof system formalized in the LFSC framework that addresses some of these challenges with the use of computational side-conditions. We report results using a proof-producing version of the CVC4 SMT solver on unsatisfiable quantifier-free bit-vector benchmarks from the SMT-LIB benchmark library.
BibTeX entry:
@inproceedings{HBR+15,
author = {Liana Hadarean and Clark Barrett and Andrew Reynolds and
Cesare Tinelli and Morgan Deters},
editor = {Martin Davis and Ansgar Fehnker and Annabelle McIver and
Andrei Voronkov},
title = {Fine-grained {SMT} Proofs for the Theory of Fixed-width
Bit-vectors},
booktitle = {Proceedings of the {\it 20^{th}} International Conference
on Logic for Programming, Artificial Intelligence, and Reasoning
(LPAR '15)},
series = {Lecture Notes in Computer Science},
volume = {9450},
pages = {340--355},
publisher = {Springer},
month = nov,
year = {2015},
note = {Suva, Fiji},
url = {http://theory.stanford.edu/~barrett/pubs/HBR+.pdf}
}
(This webpage was created with bibtex2web.)