Sciweavers

Share
ATVA
2009
Springer

Automated Analysis of Data-Dependent Programs with Dynamic Memory

9 years 1 months ago
Automated Analysis of Data-Dependent Programs with Dynamic Memory
We present a new approach for automatic verification of data-dependent programs manipulating dynamic heaps. A heap is encoded by a graph where the nodes represent the cells, and the edges reflect the pointer structure between the cells of the heap. Each cell contains a set of variables which range over the natural numbers. Our method relies on standard backward reachability analysis, where the main idea is to use a simple set of predicates, called signatures, in order to represent bad sets of heaps. Examples of bad heaps are those which contain either garbage, lists which are not well-formed, or lists which are not sorted. We present the results for the case of programs with a single next-selector, and where variables may be compared for (in)equality. This allows us to verify for instance that a program, like bubble sort or insertion sort, returns a list which is well-formed and sorted, or that the merging of two sorted lists is a new sorted list. We report on the result of running a...
Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederbe
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ATVA
Authors Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji
Comments (0)
books