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.

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