Fine grained SMT proofs for the theory of fixed-width bit-vectors

Liana Hadarean, Clark Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings
EditorsAndrei Voronkov, Ansgar Fehnker, Martin Davis, Annabelle McIver
PublisherSpringer Verlag
Pages340-355
Number of pages16
ISBN (Print)9783662488980
DOIs
StatePublished - 2015
Event20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 - Suva, Fiji
Duration: Nov 24 2015Nov 28 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9450
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015
CountryFiji
CitySuva
Period11/24/1511/28/15

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Fine grained SMT proofs for the theory of fixed-width bit-vectors'. Together they form a unique fingerprint.

Cite this