一句话：提出弱公理化乘法的非线性算术理论及后承发现算法，用于生成循环不变式并证明程序安全性质。
本文研究非线性整数/实数算术的自动推理问题。作者将线性算术扩展为一个乘法符号仅弱公理化的理论，从而保留线性算术的若干良好算法性质，并证明其合取片段可像凸多面体运算一样被有效操作。基于此，论文求解后承发现问题：给定基公式 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.
@article{paperbot2117,
title = {When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic},
author = {Zachary Kincaid and Nicolas Koh and Shaowei Zhu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571237}
}