English

Loop Summarization with Rational Vector Addition Systems (extended version)

Programming Languages 2019-07-16 v2

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.

Keywords

Cite

@article{arxiv.1905.06495,
  title  = {Loop Summarization with Rational Vector Addition Systems (extended version)},
  author = {Jake Silverman and Zachary Kincaid},
  journal= {arXiv preprint arXiv:1905.06495},
  year   = {2019}
}
R2 v1 2026-06-23T09:08:09.821Z