Loop Summarization with Rational Vector Addition Systems (extended version)

Abstract

This paper presents a technique for computing numerical loop summaries. The method works first synthesizing a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then using the (polytime computable) reachability relation of Q-VASRs to over-approximate the behavior of the loop. The key technical problem solved in this paper is to synthesize a Q-VASR that is a best abstraction of a loop in the sense that (1) it simulates the loop and (2) it is simulated by any other Q-VASR that simulates the loop. As a result, our loop summarization scheme has predictable precision. We implement the summarization algorithm and show experimentally that it is precise and performant.