Underapproximation of procedure summaries for integer programs
From MaRDI portal
Publication:5326329
DOI10.1007/978-3-642-36742-7_18zbMATH Open1381.68052arXiv1210.4289OpenAlexW2338346238MaRDI QIDQ5326329FDOQ5326329
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)
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.
Full work available at URL: https://arxiv.org/abs/1210.4289
Recommendations
Cited In (6)
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)
