Loop summarization with rational vector addition systems

Jake Silverman, Zachary Kincaid

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

1 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
PublisherSpringer Verlag
Pages97-115
Number of pages19
ISBN (Print)9783030255428
DOIs
StatePublished - Jan 1 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

Conference

Conference31st International Conference on Computer Aided Verification, CAV 2019
CountryUnited States
CityNew York City
Period7/15/197/18/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Silverman, J., & Kincaid, Z. (2019). Loop summarization with rational vector addition systems. In I. Dillig, & S. Tasiran (Eds.), Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings (pp. 97-115). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11562 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-25543-5_7