### 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 language | English (US) |
---|---|

Title of host publication | Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Proceedings |

Publisher | Springer Verlag |

Pages | 340-355 |

Number of pages | 16 |

Volume | 9450 |

ISBN (Print) | 9783662488980 |

DOIs | |

State | Published - 2015 |

Event | 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 - Suva, Fiji Duration: Nov 24 2015 → Nov 28 2015 |

### Publication series

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

Volume | 9450 |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Other

Other | 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015 |
---|---|

Country | Fiji |

City | Suva |

Period | 11/24/15 → 11/28/15 |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Theoretical Computer Science

### Cite this

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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 -