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.