Conference proceeding
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
Logic for programming, artificial intelligence, and reasoning. 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015 : proceedings, Vol.9450, pp.340-355
Lecture Notes in Computer Science, 1st ed. 2015
LPAR, 20th (Suva, Fiji)
2015
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 SMT-generated 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.
Details
- Title: Subtitle
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
- Creators
- Liana HadareanClark BarrettAndrew ReynoldsCesare Tinelli - University of Iowa, Computer ScienceMorgan Deters
- Resource Type
- Conference proceeding
- Publication Details
- Logic for programming, artificial intelligence, and reasoning. 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015 : proceedings, Vol.9450, pp.340-355
- Conference
- LPAR, 20th (Suva, Fiji)
- Edition
- 1st ed. 2015
- Publisher
- Springer; Heidelberg
- Series
- Lecture Notes in Computer Science
- ISSN
- 0302-9743
- eISSN
- 1611-3349
- Grant note
- Work partially supported by DARPA award FA8750-13-2-0241 and ERC project 280053 (CPROVER).
- Language
- English
- Date published
- 2015
- Academic Unit
- Computer Science
- Record Identifier
- 9984002320202771
Metrics
16 Record Views