Loop summarization with rational vector addition systems

DOI10.1007/978-3-030-25543-5_7MaRDI QIDQ6154875zbMATH OpenOpenAlexFDO

Authors Jake Silverman, Zachary Kincaid

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1905.06495

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Loop Summarization and Termination Analysis
• Loop summarization using state and transition invariants
• Loop Summarization Using Abstract Transformers
• Abstract acceleration of general linear loops
• A Lightweight Approach for Loop Summarization

Cited in

(1)

• Reflections on termination of linear loops

This page was built for publication: Loop summarization with rational vector addition systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154875)