Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
复制标题
可解多项式理想：程序分析的理想反映
DOI：
10.1145/3632867
复制
发表时间：
2024
影响因子：
--
通讯作者：
Kincaid, Zachary
中科院分区：
文献类型：
--
作者：
Cyphert, John;Kincaid, Zachary
本文提出了一种程序分析方法，生成涉及多项式算术的程序摘要。我们的方法建立在以前的技术，使用可解多项式映射总结循环。这些技术是能够生成所有多项式不变式的一类受限制的程序，但不能被应用到这个类以外的程序-例如，程序与嵌套循环，条件分支，非结构化控制流等，目前缺乏的方法来应用这些先前的方法的情况下，一般的程序。本文填补了这一空白。我们的方法不是限制我们可以处理的程序的种类，而是将每个循环抽象成一个可以用现有技术解决的模型，从而将可解多项式映射的工作带到一般程序中。虽然没有任何方法可以产生所有的多项式不变量的任意程序，我们的方法建立了它的优点，通过单调性的结果。我们已经实现了我们的技术，并测试了一套基准从文献。我们的实验表明，我们的技术显示出具有挑战性的验证任务，需要非线性推理的承诺。
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.
登录
查看更多内容
对线性循环终止的思考
DOI：
10.1007/978-3-030-81688-9_3
发表时间：
2021
期刊：
Computer Aided Verification
影响因子：
--
作者：
Zhu, Shaowei;Kincaid, Zachary
通讯作者：
Kincaid, Zachary
DOI：
10.1145/3209108.3209142
发表时间：
2018-02
期刊：
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
E. Hrushovski;Joël Ouaknine;Amaury Pouly;J. Worrell
通讯作者：
E. Hrushovski;Joël Ouaknine;Amaury Pouly;J. Worrell
关于最强代数程序不变量
影响因子：
2.5
作者：
Hrushovski E
通讯作者：
Hrushovski E
使用有理向量加法系统进行循环汇总（扩展版）
DOI：
10.1007/978-3-030-25543-5_7
发表时间：
2019
期刊：
ArXiv
影响因子：
--
作者：
Jake Silverman;Zachary Kincaid
通讯作者：
Zachary Kincaid
DOI：
10.1145/3410313
发表时间：
2021
期刊：
Artifact Digital Object Group
影响因子：
--
作者：
Shaowei Zhu;Zachary Kincaid
通讯作者：
Zachary Kincaid