When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
复制标题
DOI：
10.1145/3571237
复制
发表时间：
2022-11
影响因子：
--
通讯作者：
Zachary Kincaid;Nicolas C. H. Koh;Shaowei Zhu
中科院分区：
文献类型：
--
作者：
Zachary Kincaid;Nicolas C. H. Koh;Shaowei Zhu
本文提出了一种非线性整数/真实的算术的理论，并给出了该理论的推理算法。该理论可以被认为是线性整数/真实的算术的扩展，具有弱公理化的乘法符号，它保留了线性算术的许多理想的算法性质。特别是，我们证明了理论的合取片段可以有效地操作（类似于凸多面体上的通常操作，线性算术的合取片段）。结果，我们可以解决以下结果发现问题：给定一个基础公式F，找到F所蕴涵的最强合取公式。作为结果发现的一个应用，我们给出了一个循环不变式生成算法，该算法在理论上是单调的，并且在某种意义上是完备的。实验表明，从结果生成的不变量是有效的证明程序的安全性，需要非线性推理。
This paper presents a theory of non-linear integer/real arithmetic and algorithms for reasoning about this theory. The theory can be conceived of as an extension of linear integer/real arithmetic with a weakly-axiomatized multiplication symbol, which retains many of the desirable algorithmic properties of linear arithmetic. In particular, we show that the conjunctive fragment of the theory can be effectively manipulated (analogously to the usual operations on convex polyhedra, the conjunctive fragment of linear arithmetic). As a result, we can solve the following consequence-finding problem: given a ground formula F, find the strongest conjunctive formula that is entailed by F. As an application of consequence-finding, we give a loop invariant generation algorithm that is monotone with respect to the theory and (in a sense) complete. Experiments show that the invariants generated from the consequences are effective for proving safety properties of programs that require non-linear reasoning.