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.|
|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|
|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.