@inproceedings{d27071e10185416d93c566a4f8128090,
title = "Loop summarization with rational vector addition systems",
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.",
author = "Jake Silverman and Zachary Kincaid",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2019.; 31st International Conference on Computer Aided Verification, CAV 2019 ; Conference date: 15-07-2019 Through 18-07-2019",
year = "2019",
doi = "10.1007/978-3-030-25543-5_7",
language = "English (US)",
isbn = "9783030255428",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "97--115",
editor = "Isil Dillig and Serdar Tasiran",
booktitle = "Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings",
address = "Germany",
}