  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.
