“IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL” by Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli. In Proceedings of the 30^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '24), (Bernd Finkbeiner and Laura Kovács, eds.), Apr. 2024, pp. 311-330. Luxembourg City, Luxembourg.
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.
BibTeX entry:
@inproceedings{LFA+24,
author = {Hanna Lachnitt and Mathias Fleury and Leni Aniva and Andrew
Reynolds and Haniel Barbosa and Andres N{\"o}tzli and Clark
Barrett and Cesare Tinelli},
editor = {Bernd Finkbeiner and Laura Kov{\'a}cs},
title = {{IsaRare}: Automatic Verification of {SMT} Rewrites in
{Isabelle/HOL}},
booktitle = {Proceedings of the {\it 30^{th}} International Conference
on Tools and Algorithms for the Construction and Analysis of
Systems (TACAS '24)},
series = {Lecture Notes in Computer Science},
volume = {14570},
pages = {311--330},
publisher = {Springer},
month = apr,
year = {2024},
doi = {10.1007/978-3-031-57246-3_17},
note = {Luxembourg City, Luxembourg},
url = {http://theory.stanford.edu/~barrett/pubs/LFA+24.pdf}
}
(This webpage was created with bibtex2web.)