Loop summarization with rational vector addition systems

DOI10.1007/978-3-030-25543-5_7arXiv1905.06495OpenAlexW2956274457MaRDI QIDQ6154875FDOQ6154875

Authors: Jake Silverman, Zachary Kincaid 

Publication date: 16 February 2024

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

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.

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

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

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)

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)