Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/s10009-016-0420-7 | STTT |
Keywords | DocType | Volume |
similar result,precise summary relation,recursive program,recursive case,integer program,original recursive program,non-recursive program,off-the-shelf analyzer,procedure summary,method terminates | Conference | 19 |
Issue | ISSN | Citations |
5 | 1433-2787 | 4 |
PageRank | References | Authors |
0.43 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pierre Ganty | 1 | 242 | 20.29 |
| Radu Iosif | 2 | 483 | 42.44 |
| Filip Konečný | 3 | 83 | 3.78 |