=Paper=
{{Paper
|id=Vol-3429/abstract14
|storemode=property
|title=Automatic Verification of SMT Rewrites in Isabelle/HOL
|pdfUrl=https://ceur-ws.org/Vol-3429/abstract14.pdf
|volume=Vol-3429
|authors=Hanna Lachnitt,Mathias Fleury,Leni Aniva,Andrew Reynolds,Haniel Barbosa,Andres Noetzli,Clark Barrett,Cesare Tinelli
|dblpUrl=https://dblp.org/rec/conf/smt/LachnittFA0BNBT23
}}
==Automatic Verification of SMT Rewrites in Isabelle/HOL==
<pdf width="1500px">https://ceur-ws.org/Vol-3429/abstract14.pdf</pdf>
<pre>
Abstract: Automatic Verification of SMT Rewrites in
Isabelle/HOL
Hanna Lachnitt1 , Mathias Fleury2 , Leni Aniva1 , Andrew Reynolds3 , Haniel Barbosa4 ,
Andres Noetzli5 , Clark Barrett1 and Cesare Tinelli3
1
  Stanford University
2
  University of Freiburg
3
  The University of Iowa
4
  Universidade Federal de Minas Gerais
5
  Cubist, Inc.


                                         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 proof certificates, which record the reasoning steps the solver has done.
                                         These proof certificates can be given to a proof checker which determines whether the steps in the
                                         proof are correct. One key challenge with this approach is that it is difficult to efficiently and accurately
                                         produce proofs for reasoning steps involving term rewriting rules (of which there are many in modern
                                         SMT solvers). Previous work showed how a domain-specific language, RARE, can be used to capture
                                         rewriting rules for the purposes of proof production. However, the RARE rules were trusted—i.e., the
                                         correctness of the rules themselves was not checked by the proof checker. In this paper, we present
                                         IsaRARE, a tool that can automatically generate lemmas in the interactive theorem prover Isabelle/HOL
                                         corresponding to RARE rewrite rules. The correctness of the rules can then be verified by proving the
                                         lemmas. We evaluate our approach by verifying an extensive set of rewrite rules used by the cvc5 SMT
                                         solver.




 SMT’23: 21st International Workshop on Satisfiability Modulo Theories, July 5–6, 2023, Rome, Italy
$ lachnitt@stanford.edu (H. Lachnitt); fleury@cs.uni-freiburg.de (M. Fleury); leniv@stanford.edu (L. Aniva);
andrew-reynolds@uiowa.edu (A. Reynolds); hbarbosa@dcc.ufmg.br (H. Barbosa); noetzli@cs.stanford.edu
(A. Noetzli); barrett@cs.stanford.edu (C. Barrett); cesare-tinelli@uiowa.edu (C. Tinelli)
                                       © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)

</pre>