论文标题
当较少的时间时：算术理论中的后果调查
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
论文作者
论文摘要
本文提出了一种非线性整数/真实算术和算法的理论，用于推理该理论。该理论可以被认为是线性整数/真实算术的扩展，并具有弱轴化的乘法符号，该符号保留了线性算术的许多理想算法属性。特别是，我们表明该理论的结合片段可以有效地操纵（类似于对凸多面体的通常操作，即线性算术的结合片段）。结果，我们可以解决以下结果发现问题：鉴于地面公式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 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.
