Loop summarization with rational vector addition systems

Jake Silverman, Zachary Kincaid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
PublisherSpringer Verlag
Number of pages19
ISBN (Print)9783030255428
StatePublished - 2019
Event31st International Conference on Computer Aided Verification, CAV 2019 - New York City, United States
Duration: Jul 15 2019Jul 18 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11562 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference31st International Conference on Computer Aided Verification, CAV 2019
Country/TerritoryUnited States
CityNew York City

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Loop summarization with rational vector addition systems'. Together they form a unique fingerprint.

Cite this