一句话：将任意循环抽象为可解多项式映射模型，从而把循环多项式不变式生成技术推广到一般程序。
已有基于可解多项式映射的循环摘要技术只能为一类受限程序生成全部多项式不变式，无法处理嵌套循环、条件分支、非结构化控制流等一般程序。本文不限制可处理的程序种类，而是通过「理想反射」把每个循环抽象成可用既有技术求解的模型，从而将可解多项式映射的工作推广到一般程序。由于任何方法都无法为任意程序生成全部多项式不变式，作者提出单调性结果来刻画该方法的合理性。作者实现了相应技术，并在文献中的基准程序集上进行了测试，实验表明该方法在需要非线性推理的困难验证任务上具有潜力。
This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to generate all polynomial invariants for a restricted class of programs, but cannot be applied to programs outside of this class—for instance, programs with nested loops, conditional branching, unstructured control flow, etc. There currently lacks approaches to apply these prior methods to the case of general programs. This paper bridges that gap. Instead of restricting the kinds of programs we can handle, our method abstracts every loop into a model that can be solved with prior techniques, bringing to bear prior work on solvable polynomial maps to general programs. While no method can generate all polynomial invariants for arbitrary programs, our method establishes its merit through a monotonicty result. We have implemented our techniques, and tested them on a suite of benchmarks from the literature. Our experiments indicate our techniques show promise on challenging verification tasks requiring non-linear reasoning.
@article{paperbot2618,
title = {Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis},
author = {John Cyphert and Zachary Kincaid},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632867}
}