Skip to main content

Loop Summarization with Rational Vector Addition Systems

Author(s): Silverman, Jake; Kincaid, Zachary

To refer to this page use:
Abstract: This paper presents a technique for computing numerical loop summaries. The method synthesizes a rational vector addition system with resets ( ℚ -VASR) that simulates the action of an input loop, and then uses the reachability relation of that ℚ -VASR to over-approximate the behavior of the loop. The key technical problem solved in this paper is to automatically synthesize a ℚ -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 ℚ -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.
Publication Date: 2019
Citation: Silverman, Jake, and Zachary Kincaid. "Loop Summarization with Rational Vector Addition Systems." In International Conference on Computer Aided Verification (2019): pp. 97-115. doi:10.1007/978-3-030-25543-5_7
DOI: 10.1007/978-3-030-25543-5_7
ISSN: 0302-9743
Pages: 97 - 115
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Computer Aided Verification
Version: Final published version. Article is made available in OAR by the publisher's permission or policy.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.