“Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language” by Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 22^nd International Conference on Formal Methods In Computer-Aided Design (FMCAD '22), (Alberto Griggio and Neha Rungta, eds.), Oct. 2022, pp. 65-74.
Satisfiability modulo theories (SMT) solvers are widely used to prove security and safety properties of computer systems. For these applications, it is crucial that the result reported by an SMT solver be correct. Recently, there has been a renewed focus on producing independently checkable proofs in SMT solvers, partly with the aim of addressing this risk. These proofs record the reasoning done by an SMT solver and are ideally detailed enough to be easy to check. At the same time, modern SMT solvers typically implement hundreds of different term-rewriting rules in order to achieve state-of-the-art performance. Generating detailed proofs for applications of these rules is a challenge, because code implementing rewrite rules can be large and complex. Instrumenting this code to additionally produce proofs makes it even more complex and makes it harder to add new rewrite rules. We propose an alternative approach to the direct instrumentation of the rewriting module of an SMT solver. The approach uses a domain-specific language (DSL) to describe a set of rewrite rules declaratively and then reconstructs detailed proofs for specific rewrite steps on demand based on those declarative descriptions.
BibTeX entry:
@inproceedings{NBN+22,
author = {Andres N{\"o}tzli and Haniel Barbosa and Aina Niemetz and
Mathias Preiner and Andrew Reynolds and Clark Barrett and Cesare
Tinelli},
editor = {Alberto Griggio and Neha Rungta},
title = {Reconstructing Fine-Grained Proofs of Rewrites Using a
Domain-Specific Language},
booktitle = {Proceedings of the {\it 22^{nd}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '22)},
pages = {65--74},
publisher = {TU Wien Academic Press},
month = oct,
year = {2022},
doi = {10.34727/2022/isbn.978-3-85448-053-2_12},
url = {http://theory.stanford.edu/~barrett/pubs/NBN+22.pdf}
}
(This webpage was created with bibtex2web.)