Underapproximation of procedure summaries for integer programs

DOI10.1007/978-3-642-36742-7_18MaRDI QIDQ5326329zbMATH OpenOpenAlexFDO

Authors Pierre Ganty, Radu Iosif, Filip Konečný

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We show how to underapproximate the procedure summaries of recursive programs over the integers using off-the-shelf analyzers for non-recursive programs. The novelty of our approach is that the non-recursive program we compute may capture unboundedly many behaviors of the original recursive program for which stack usage cannot be bounded. Moreover, we identify a class of recursive programs on which our method terminates and returns the precise summary relations without underapproximation. Doing so, we generalize a similar result for non-recursive programs to the recursive case. Finally, we present experimental results of an implementation of our method applied on a number of examples.

Recommendations

• Computing Procedure Summaries for Interprocedural Analysis
• Programming Languages and Systems
• Summarization for termination: No return!
• Summarizing procedures in concurrent programs
• Generating precise and concise procedure summaries

Cited in

(6)

• Programming Languages and Systems
• scientific article; zbMATH DE number 7439739 (Why is no real title available?)
• Interprocedural reachability for flat integer programs
• Solving non-linear Horn clauses using a linear Horn clause solver
• A calculus for modular loop acceleration
• Predicate pairing for program verification

This page was built for publication: Underapproximation of procedure summaries for integer programs

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