Book chapter
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
Tools and Algorithms for the Construction and Analysis of Systems, pp.311-330
Lecture Notes in Computer Science, v. 14570, Springer Nature Switzerland
2024
DOI: 10.1007/978-3-031-57246-3_17
Abstract
Satisfiability modulo theories (SMT) solvers are widely used to ensure the correctness of safety- and security-critical applications. Therefore, being able to trust a solver’s results is crucial. One way to increase trust is to generate independently checkable proof certificates, which record the reasoning steps done by the solver. A key challenge with this approach is that it is difficult to efficiently and accurately produce proofs for reasoning steps involving term rewriting rules. Previous work showed how a domain-specific language, Rare, can be used to capture rewriting rules for the purposes of proof production. However, in that work, the Rare rules had to be trusted, as the correctness of the rules themselves was not checked by the proof checker. In this paper, we present IsaRare, a tool that can automatically translate Rare rules into Isabelle/HOL lemmas. The soundness of the rules can then be verified by proving the lemmas. Because an incorrect rule can put the entire soundness of a proof system in jeopardy, our solution closes an important gap in the trustworthiness of SMT proof certificates. The same tool also provides a necessary component for enabling full proof reconstruction of SMT proof certificates in Isabelle/HOL. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT solver.
Details
- Title: Subtitle
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
- Creators
- Hanna Lachnitt - Stanford UniversityMathias Fleury - University of FreiburgLeni Aniva - Stanford UniversityAndrew Reynolds - University of IowaHaniel Barbosa - Universidade Federal de Minas GeraisAndres Nötzli - Cubist PharmaceuticalsClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Tools and Algorithms for the Construction and Analysis of Systems, pp.311-330
- Publisher
- Springer Nature Switzerland; Cham
- Series
- Lecture Notes in Computer Science; v. 14570
- DOI
- 10.1007/978-3-031-57246-3_17
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2024
- Academic Unit
- Computer Science
- Record Identifier
- 9984622896802771
Metrics
1 Record Views