Loop Summarization with Rational Vector Addition Systems

Abstract

This paper presents a technique for computing numerical loop summaries. The method synthesizes a rational vector addition system with resets ( $$\mathbb {Q}$$ -VASR) that simulates the action of an input loop, and then uses the reachability relation of that $$\mathbb {Q}$$ -VASR to over-approximate the behavior of the loop. The key technical problem solved in this paper is to automatically synthesize a $$\mathbb {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 $$\mathbb {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.