Résumé | 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.
Joint work with Pierre Ganty (IMDEA) and Filip Konecny (EPFL). |