Verification of Programs Manipulating Complex Dynamic Data Structures

We develop a verication method based on a novel useof tree automata to represent heap congurations to al-low verication of important properties|such as no null-pointer dereferences, absence of memory leaks, etc.|forprograms manipulating complex dynamically linked datastructures. In our approach, a heap is split into sev-eral separated" parts such that each of them can berepresented by a tree automaton. The automata canrefer to each other allowing the dierent parts of theheaps to mutually refer to their boundaries. Moreover,we allow for a hierarchical representation of heaps by al-lowing alphabets of the tree automata to contain other,nested tree automata. Program instructions can be eas-ily encoded as operations on our representation struc-ture. This allows verication of programs based on sym-bolic state-space exploration together with renable ab-straction within the so-called abstract regular tree modelchecking. A motivation for the approach is to combine ad-vantages of automata-based approaches (higher generalityand exibility of the abstraction) with some advantagesof separation-logic-based approaches (eciency).