Loop Summarization with Rational Vector Addition Systems (extended version)

TL;DR

This paper introduces a novel method for automatically synthesizing the most precise rational vector addition system with resets (Q-VASR) to over-approximate loop behavior, providing theoretical guarantees and demonstrating practical effectiveness.

Contribution

It presents a new technique for synthesizing the best abstraction of a loop using Q-VASR, enabling precise and guaranteed loop summaries.

Findings

The method accurately over-approximates loop behavior.

It provides theoretical guarantees about the summaries.

Experimental results show high precision and efficiency.

Abstract

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.