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
PublisherSpringer Verlag
Pages340-355
Number of pages16
Volume9450
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Surface mount technology
Quantifiers
Benchmark
Proof System
Propositional Logic
Certificate
Correctness
Encoding
Assignment

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Hadarean, L., Barrett, C., Reynolds, A., Tinelli, C., & Deters, M. (2015). Fine grained SMT proofs for the theory of fixed-width bit-vectors. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings (Vol. 9450, pp. 340-355). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9450). Springer Verlag. https://doi.org/10.1007/978-3-662-48899-7_24

Fine grained SMT proofs for the theory of fixed-width bit-vectors. / Hadarean, Liana; Barrett, Clark; Reynolds, Andrew; Tinelli, Cesare; Deters, Morgan.

Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings. Vol. 9450 Springer Verlag, 2015. p. 340-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9450).

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

Hadarean, L, Barrett, C, Reynolds, A, Tinelli, C & Deters, M 2015, Fine grained SMT proofs for the theory of fixed-width bit-vectors. in Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings. vol. 9450, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9450, Springer Verlag, pp. 340-355, 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015, Suva, Fiji, 11/24/15. https://doi.org/10.1007/978-3-662-48899-7_24
Hadarean L, Barrett C, Reynolds A, Tinelli C, Deters M. Fine grained SMT proofs for the theory of fixed-width bit-vectors. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings. Vol. 9450. Springer Verlag. 2015. p. 340-355. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-48899-7_24
Hadarean, Liana ; Barrett, Clark ; Reynolds, Andrew ; Tinelli, Cesare ; Deters, Morgan. / 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, Proceedings. Vol. 9450 Springer Verlag, 2015. pp. 340-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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",
year = "2015",
doi = "10.1007/978-3-662-48899-7_24",
language = "English (US)",
isbn = "9783662488980",
volume = "9450",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "340--355",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings",

}

TY - GEN

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

AU - Hadarean, Liana

AU - Barrett, Clark

AU - Reynolds, Andrew

AU - Tinelli, Cesare

AU - Deters, Morgan

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84952668317&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84952668317&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-48899-7_24

DO - 10.1007/978-3-662-48899-7_24

M3 - Conference contribution

AN - SCOPUS:84952668317

SN - 9783662488980

VL - 9450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 340

EP - 355

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

PB - Springer Verlag

ER -