Underapproximation of Procedure Summaries for Integer Programs

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...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2016-04
Main Authors: Ganty, Pierre, Iosif, Radu, Konečný, Filip
Format: Article
Language:English
Subjects:
Computation and Language
Computer Science
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 re-cursive case. Finally, we present experimental results of an implementation of our method applied on a number of examples.
ISSN:1433-2779
1433-2787