Under approximation of Procedure Summaries for Integer Programs

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