| TR#: | CS-2000-09 |
| Class: | CS |
| Title: | Interprocedual Shape Analysis for Recursive Programs |
| Authors: | Noam Rinetzky, Mooly Sagiv
|
| CS-2000-09.pdf | |
| Abstract: | A shape-analysis algorithm statically analyzes a program to determine information about the heap-allocated data structures that the program manipulates. The results can be used to optimize, understand, debug or verify programs. Existing algorithms are quite imprecise in the presence of recursive procedure calls. This is unfortunate, since recursion provides a natural way to manipulate linked data structures. We present a novel technique for shape analysis of recursive programs. An algorithm based on our technique was implemented. It handles programs manipulating linked lists written in a subset of C. The algorithm is significantly more precise than existing algorithms. For example, it can verify the absence of memory leaks in many recursive programs, which is beyond the scope of existing algorit |
| Copyright | The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information |
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2000/CS/CS-2000-09), rather than to the URL of the PDF files directly. The latter URLs may change without notice.
To the list of the CS technical reports of 2000
To the main CS technical reports page