按需量词
Quantifiers on Demand
摘要：
自动程序验证是一个难题。即使对于线性代数上的转移系统，它也是不可判定的。用数组理论扩展转换系统，通过要求用普遍量化的公式进行推理和推理，使问题进一步复杂化。在本文中，我们提出了一个新的算法，Quic3，扩展IC3推断普遍量化的不变量的LIA和数组的组合理论。与其他使用IC3或SMT求解器作为黑盒的方法不同，Quic3仔细管理量化泛化（以构建量化不变量）和量词实例化（以检测量词存在时的收敛性）。虽然Quic3不能保证收敛，但它可以保证通过探索越来越长的执行来取得进展。我们在Z3的约束Horn子句求解器引擎中实现了Quic3，并通过应用Quic3来验证数组操作C程序的各种公共基准来进行实验。
英文摘要：
Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, Quic3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, Quic3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While Quic3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented Quic3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying Quic3 to verifying a variety of public benchmarks of array manipulating C programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
