Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
复制标题
DOI：
10.1145/3573105.3575674
复制
发表时间：
2023-01
期刊：
影响因子：
--
通讯作者：
M. Daggitt;R. Atkey;Wen Kokke;Ekaterina Komendantskaya;Luca Arnaboldi-
中科院分区：
文献类型：
--
作者：
M. Daggitt;R. Atkey;Wen Kokke;Ekaterina Komendantskaya;Luca Arnaboldi-
现代验证工具经常依赖于将高级规范编译为 SMT 查询。然而，高级规范语言通常比可用的求解器更具表现力，因此该工具必须拒绝一些语法上有效的规范。在这种情况下，面临的挑战是向用户提供可理解的错误消息，将规范的原始语法形式与其被拒绝的语义原因联系起来。在本文中，我们演示了如何通过将基于标准统一的类型检查器与类型类和自动泛化相结合来执行此分析。具体来说，类型检查被用作一种构造性过程，用于低估给定的规范是否属于求解器支持的问题子集。任何由此产生的拒绝证据都可以转化为对用户的详细解释。该方法是组合的，不需要用户向其程序添加额外的键入注释。随后，我们描述了如何利用类型系统来提供从适当类型的表达式到 SMT 查询的健全且完整的编译过程，我们已在 Agda 中对此进行了验证。
Modern verification tools frequently rely on compiling high-level specifications to SMT queries. However, the high-level specification language is usually more expressive than the available solvers and therefore some syntactically valid specifications must be rejected by the tool. In such cases, the challenge is to provide a comprehensible error message to the user that relates the original syntactic form of the specification to the semantic reason it has been rejected. In this paper we demonstrate how this analysis may be performed by combining a standard unification-based type-checker with type classes and automatic generalisation. Concretely, type-checking is used as a constructive procedure for under-approximating whether a given specification lies in the subset of problems supported by the solver. Any resulting proof of rejection can be transformed into a detailed explanation to the user. The approach is compositional and does not require the user to add extra typing annotations to their program. We subsequently describe how the type system may be leveraged to provide a sound and complete compilation procedure from suitably typed expressions to SMT queries, which we have verified in Agda.