Conference proceeding
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language
2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, Vol.3, pp.65-74
Formal Methods in Computer-Aided Design
01/01/2022
DOI: 10.34727/2022/isbn.978-3-85448-053-2_12
Abstract
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.
Details
- Title: Subtitle
- Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language
- Creators
- Andres Notzli - Stanford UniversityHaniel Barbosa - Federal ReserveAina Niemetz - Stanford UniversityMathias Preiner - Stanford UniversityAndrew Reynolds - Univ Iowa, Iowa City, IA USAClark Barrett - Stanford UniversityCesare Tinelli - Univ Iowa, Iowa City, IA USA
- Contributors
- A Griggio (Editor)N Rungta (Editor)
- Resource Type
- Conference proceeding
- Publication Details
- 2022 FORMAL METHODS IN COMPUTER-AIDED DESIGN, FMCAD, Vol.3, pp.65-74
- Series
- Formal Methods in Computer-Aided Design
- DOI
- 10.34727/2022/isbn.978-3-85448-053-2_12
- Publisher
- TU Wien Acad Press
- Number of pages
- 10
- Grant note
- FA8650-18-27861 / DARPA; United States Department of Defense; Defense Advanced Research Projects Agency (DARPA) Stanford Agile Hardware Center
- Language
- English
- Date published
- 01/01/2022
- Academic Unit
- Computer Science
- Record Identifier
- 9984480136602771
Metrics
13 Record Views