用于Horn-Clause验证的析取插值（扩展技术报告）
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
摘要：
在软件验证的主要挑战之一是有效和精确的程序与过程和循环的组合分析。插值方法仍然是最有前途的技术之一，这样的验证，是密切相关的解决霍恩子句约束。我们引入了一个新的概念插值，析取插值，解决了更一般的一类问题，在一个步骤相比，以前的概念插值，如树插值或归纳序列的插值。我们目前的算法和复杂性建设的析取插值，以及它们的使用内的抽象细化循环。我们已经实现了霍恩条款验证算法，使用析取插值和评估他们的基准表示为霍恩条款的整数线性算术理论。
英文摘要：
One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remain one of the most promising techniques for such verification, and are closely related to solving Horn clause constraints. We introduce a new notion of interpolation, disjunctive interpolation, which solve a more general class of problems in one step compared to previous notions of interpolants, such as tree interpolants or inductive sequences of interpolants. We present algorithms and complexity for construction of disjunctive interpolants, as well as their use within an abstraction-refinement loop. We have implemented Horn clause verification algorithms that use disjunctive interpolants and evaluate them on benchmarks expressed as Horn clauses over the theory of integer linear arithmetic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
