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.

翻译：本文提出了一种程序分析方法，能够生成涉及多项式运算的程序摘要。我们的方法建立在先前利用可解多项式映射总结循环的技术之上。这些技术能够为受限程序类生成所有多项式不变量，但无法应用于该类别之外的程序（例如，包含嵌套循环、条件分支、非结构化控制流等的程序）。目前缺乏将这些先前方法应用于通用程序的方法。本文填补了这一空白。我们的方法不限制可处理的程序类型，而是将每个循环抽象为可通过先前技术求解的模型，从而将可解多项式映射的先前工作应用于通用程序。尽管没有任何方法能为任意程序生成所有多项式不变量，我们的方法通过单调性结果确立了其价值。我们已实现所提技术，并在文献中的基准测试集上进行了验证。实验表明，我们的技术在需要非线性推理的挑战性验证任务中展现出潜力。