@inproceedings{d4f4292a2993401692c6b729949e6b5e,

title = "Fine grained SMT proofs for the theory of fixed-width bit-vectors",

abstract = "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 SMTgenerated proofs for the quantifier-free theory of fixed-width bit-vectors. 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.",

author = "Liana Hadarean and Clark Barrett and Andrew Reynolds and Cesare Tinelli and Morgan Deters",

note = "Funding Information: Work partially supported by DARPA award FA8750-13-2-0241 and ERC project 280053 (CPROVER). Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2015.; 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 ; Conference date: 24-11-2015 Through 28-11-2015",

year = "2015",

doi = "10.1007/978-3-662-48899-7_24",

language = "English (US)",

isbn = "9783662488980",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "340--355",

editor = "Andrei Voronkov and Ansgar Fehnker and Martin Davis and Annabelle McIver",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings",

}