CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Automated Analysis of Data-Dependent Programs with Dynamic Memory

Ran Ji (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Parosh Aziz Abdulla ; Jonathan Cederberg ; Muhsin Atto
Proc. 7th International Symposium on Automated Technology for Verification and Analysis (0302-9743). Vol. 5799 (2009), Lecture Notes in Computer Science, p. 197-212.
[Konferensbidrag, refereegranskat]

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 prototype based on the method on a number of programs.



Denna post skapades 2009-12-17. Senast ändrad 2009-12-17.
CPL Pubid: 104091

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur