Loop Summarization with Rational Vector Addition Systems (extended version)
Loop Summarization with Rational Vector Addition Systems (extended version)
复制标题
使用有理向量加法系统进行循环汇总（扩展版）
DOI：
10.1007/978-3-030-25543-5_7
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Zachary Kincaid
中科院分区：
文献类型：
--
作者：
Jake Silverman;Zachary Kincaid
本文提出了一种计算数值循环求和的方法。该方法综合了一个具有重置的有理向量相加系统(Q-Vasr)，该系统模拟输入环路的动作，然后使用该Q-Vasr的可达性关系来过逼近环路的行为。本文解决的关键技术问题是自动合成Q-VASR，它是给定循环的最佳抽象，其意义在于：(1)它模拟该循环；(2)它被任何其他模拟该循环的Q-VASR所模拟。由于我们的循环摘要方案是基于计算循环的最佳抽象的精确可达关系，所以我们可以为其行为提供理论上的保证。实验结果表明，该方法具有较高的精度和实用价值。
This paper presents a technique for computing numerical loop summaries. The method synthesizes a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then uses the reachability relation of that Q-VASR to over-approximate the behavior of the loop. The key technical problem solved in this paper is to automatically synthesize a Q-VASR that is a best abstraction of a given loop in the sense that (1) it simulates the loop and (2) it is simulated by any other Q-VASR that simulates the loop. Since our loop summarization scheme is based on computing the exact reachability relation of a best abstraction of a loop, we can make theoretical guarantees about its behavior. Moreover, we show experimentally that the technique is precise and performant in practice.