Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials

Nikhil Pimpalkhare, Zachary Kincaid

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish (US)
Article number337
JournalProceedings of the ACM on Programming Languages
Volume8
Issue numberOOPSLA2
DOIs
StatePublished - Oct 8 2024

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Formal Methods
  • Invariant Generation
  • Program Analysis

Fingerprint

Dive into the research topics of 'Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials'. Together they form a unique fingerprint.

Cite this