DueList：一种面向SMT求解器的带组合子的列表理论
DueList: A Theory of Lists with Combinators for SMT Solvers
浏览论文内容
中文总结 AI 辅助
本文提出DueList，一种基于抽象-精化方法、支持任意大小列表及高阶组合子推理的SMT求解器扩展，在752个基准测试上优于Z3和CVC5，扩展了可判定问题范围。
中文摘要 AI 辅助
形式化验证工具通常依赖SMT求解器来自动推理程序，利用一系列逻辑理论（如线性整数算术、数组或字符串）来编码程序结构和验证条件。尽管近期有所进展，这些求解器在推理递归数据结构（如列表）时仍面临困难，而列表在现代函数式语言中无处不在。此外，列表常与高阶组合子结合使用，例如，将函数通用地应用于列表的所有元素。在这项工作中，我们为SMT求解器内的列表推理提供了一流支持。我们关注任意大小的列表，这些列表遵循map-reduce范式，可以仅通过一组抽象组合子进行操作。为此，我们引入了DueList，一种面向列表推理的抽象-精化方法，并将其实现在现成的SMT求解器之上。为了评估我们方法的效率，我们汇集了来自先前工作和真实世界程序的752个多样化基准测试，并将DueList与Z3和CVC5等最先进的求解器进行比较。我们的实验评估表明，DueList扩展了现有求解器的推理能力，能够判定更大范围问题的可满足性/不可满足性，同时在绝大多数先前已支持的情况下优于现有求解器。
英文摘要
Formal verification tools commonly rely on SMT solvers to automatically reason about programs, leveraging a range of logical theories, e.g., linear integer arithmetic, arrays, or strings, to encode program constructs and verification conditions. Despite recent advances, such solvers still struggle when reasoning about recursive data structures such as lists, which are pervasive in modern functional languages. Additionally, lists are commonly used in conjunction with higher-order combinators to, e.g., generically apply a function to all elements of the list. In this work, we provide first-class support for reasoning about lists within SMT solvers. We focus on lists of arbitrary size that, following the map-reduce paradigm, can be manipulated exclusively through a set of abstract combinators. To this end, we introduce DueList, an abstraction-refinement approach geared towards list reasoning, which we implement on top of off-the-shelf SMT solvers. To evaluate the efficiency of our approach, we assemble a diverse set of 752 benchmarks curated from previous works and real-world programs, and compare DueList against state-of-the-art solvers such as Z3 and CVC5. Our experimental evaluation shows that DueList extends reasoning facilities of existing solvers, allowing to conclude about the (un)satisfiability of a larger range of problems, while outperforming existing solvers in the vast majority of previously supported cases.
发表机构
- Univ. Lille, Inria, CNRS, Centrale Lille（里尔大学、法国国家信息与自动化研究所、法国国家科学研究中心、中央里尔学院）
- Inria（法国国家信息与自动化研究所）
机构由 AI 辅助整理，请以论文原文为准。
