Loop Summarization with Rational Vector Addition Systems (extended version)
Jake Silverman, Zachary Kincaid

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Parallel Computing and Optimization Techniques · Formal Methods in Verification
