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

• Type: Conference
• Year: 2009
• Where: ATVA
• Authors: Parosh Aziz Abdulla, Muhsin Atto, Jonathan Cederberg, Ran Ji
• Keywords: ATVA 2009, Data-dependent Programs, Dynamic Heaps, Hardware, Standard Backward Reachability