Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language
复制标题
使用特定于领域的语言重建细粒度的重写证明
DOI：
10.34727/2022/isbn.978-3-85448-053-2_12
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
C. Tinelli
中科院分区：
文献类型：
--
作者：
Andres Nötzli;Haniel Barbosa;Aina Niemetz;Mathias Preiner;Andrew Reynolds;Clark W. Barrett;C. Tinelli
可满足性模理论（SMT）求解器被广泛用于证明计算机系统的安全性和安全性。对于这些应用，SMT求解器报告的结果是否正确至关重要。最近，人们重新关注在SMT求解器中生成独立可检查的证明，部分目的是解决这种风险。这些证明记录了SMT求解器所做的推理，并且非常详细，易于检查。同时，现代SMT求解器通常实现数百种不同的项重写规则，以实现最先进的性能。为这些规则的应用程序生成详细的证明是一个挑战，因为实现重写规则的代码可能很大而且很复杂。插装这些代码以额外生成证明会使其变得更加复杂，并使添加新的重写规则变得更加困难。我们提出了一种替代方法的SMT求解器的重写模块的直接仪器。该方法使用域特定语言（DSL）来描述一组重写规则声明，然后重建详细的证明，根据这些声明性描述的需求，特定的重写步骤。
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.
使用工业级 SMT 求解器进行灵活的打样生产
DOI：
--
发表时间：
2022
期刊：
International Joint Conference on Automated Reasoning (IJCAR
影响因子：
--
作者：
Barbosa, Haniel;Reynolds, Andrew;Kremer, Gereon;Lachnitt, Hanna;Niemetz, Aina;Noetzli, Andres;Ozdemir, Alex;Preiner, Mathias;Viswanathan, Arjun;Viteri, Scott
通讯作者：
Viteri, Scott
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson