约束 Horn 子句的符号执行
Symbolic Execution of Constrained Horn Clauses
浏览论文内容
中文总结 AI 辅助
本文研究约束 Horn 子句的符号执行，提出约束消解演算，统一前向与后向推理，证明完备性并开发剪枝准则，实验验证于 Eldarica 求解器。
中文摘要 AI 辅助
约束 Horn 子句（CHCs）是一阶逻辑的一个片段，广泛用作验证的中间语言。我们研究约束消解作为推理 CHC 集合可满足性的演算。约束消解构成了模型检查算法（如 CEGAR 和 IC3）的简单替代方案，并在此展示出其互补特性。我们证明，当 CHCs 编码程序时，前向符号执行对应于正单元超消解，后向符号执行对应于 SLD 消解，它们是约束消解的特例。我们形式化了线性和非线性 CHCs 及转换系统的前向和后向推理，证明了在公平策略下的反驳完备性，并开发了用于剪枝冗余推导的包含准则。此外，我们展示了带包含的后向消解将 k-归纳推广到非线性 CHCs，且前向约束消解与不正确性逻辑中构造证明的问题相关。最后，我们在 Eldarica CHC 求解器上对 CHC-COMP 的基准进行了实验评估。
英文摘要
Constrained Horn clauses (CHCs) are a fragment of first-order logic widely used as an intermediate language for verification. We study constrained resolution as a calculus for reasoning about the satisfiability of sets of CHCs. Constrained resolution forms a simple alternative to model checking algorithms such as CEGAR and IC3 and is here shown to exhibit complementary features. We show that, when CHCs encode programs, forward symbolic execution corresponds to positive unit hyper-resolution, and backward symbolic execution to SLD resolution, which are special cases of constrained resolution. We formalize forward and backward reasoning for linear and non-linear CHCs and transition systems, prove refutational completeness under fair strategies, and develop subsumption criteria for pruning redundant derivations. We moreover show that backward resolution with subsumption generalizes $k$-induction to non-linear CHCs, and that forward constrained resolution is related to the problem of constructing proofs in incorrectness logic. Lastly, we provide an experimental evaluation in the Eldarica CHC solver on benchmarks from CHC-COMP.
发表机构
- TU Vienna（维也纳工业大学）
- Uppsala University（乌普萨拉大学）
- University of Regensburg（雷根斯堡大学）
机构由 AI 辅助整理，请以论文原文为准。
