---

Analyzing Heap Manipulating Programs

Verifying properties of programs manipulating the heap is an undecidable problem in general. In this talk, we will look at a few automata-theoretic approaches to analyzing properties of programs manipulating commonly used dynamically alloted data structures. Specifically, we will discuss regular model checking as a technique for reasoning about parameterized list-like data structures.

We will also look at counter automata based techniques for reasoning about lists and tree-like data structures. Finally, we will look at automata based techniques for verifying that methods operating on certain classes of data structures maintain some invariant of the data structure.