Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials

This paper presents a technique for summarizing recursive procedures operating on integer variables. The motivation of our work is to create more predictable program analyzers, and in particular to formally guarantee compositionality and monotonicity of procedure summarization. To summarize a proced...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2024-10, Vol.8 (OOPSLA2), p.1873-1899, Article 337
Main Authors: Pimpalkhare, Nikhil, Kincaid, Zachary
Format: Article
Language:English
Subjects:
Abstract machines
Program analysis
Theory of computation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a technique for summarizing recursive procedures operating on integer variables. The motivation of our work is to create more predictable program analyzers, and in particular to formally guarantee compositionality and monotonicity of procedure summarization. To summarize a procedure, we compute its best abstraction as a vector addition system with resets (VASR) and exactly summarize the executions of this VASR over the context-free language of syntactic paths through the procedure. We improve upon this technique by refining the language of syntactic paths using (automatically synthesized) linear potential functions that bound the number of recursive calls within valid executions of the input program. We implemented our summarization technique in an automated program verification tool; our experimental evaluation demonstrates that our technique computes more precise summaries than existing abstract interpreters and that our tool’s verification capabilities are comparable with state-of-the-art software model checkers.
ISSN:2475-1421
2475-1421
DOI:10.1145/3689777