Employing decision procedures for automatic program analysis and verification of heap-manipulating programs.

March 19, 2007
Greta Yorsh | Tel Aviv University

In my thesis, I developed techniques for combining automated reasoning tools e.g., theorem provers, decision procedures) with abstract interpretation and applied these techniques to programs that manipulate dynamically allocated memory.

The first part of my research provides algorithms for computing abstract representation of a set of concrete program states described by a formal specification. These algorithms rely on automated reasoning tools for extracting certain information from the specification. While these algorithms are applicable to a wide range of analysis problems, the main focus of my thesis is analysis of programs that manipulate recursive data structures, such as singly-linked lists, doubly-linked lists, trees, etc. Specifications of such programs often involve reachability properties. For example, to establish that a memory configuration contains no garbage elements, we can show that every element is reachable from some program variable. Other examples include acyclicity and disjointness of data-structures.

The second part of my research provides a way to automatically reason about interesting reachability properties, using a new decidable logic, called LRP. Automated reasoning about reachability is usually a difficult task, in particular, even simple logics become undecidable when reachability is added. Unlike these logics, LRP is both decidable and expressive enough to describe important properties of data-structures with an arbitrary number of pointer fields and of arbitrary shapes. A decision procedure for LRP can be employed in the algorithms developed in the first part of this research. This allows us, for instance, to compute abstract representation of the effect of a method call, provided that this method’s specification is expressed in LRP.

Altogether, these results provide a way to perform modular program analysis of an important class of programs that manipulate recursive data structures.

Speaker Details

Greta Yorsh is a PhD candidate in the School of Computer Science, Tel Aviv University. Her primary research interest is automatic program analysis and verification, in particular verification of imperative programs that manipulate dynamically allocated memory. Her current focus is on employing decision procedures for precise program analysis of large programs, using assume-guarantee reasoning. Her broader related interests include decidable logics for describing linked data structures, automatic generation of specifications, and software security.