%0 Journal Article
%T Verification of Programs Manipulating Complex Dynamic Data Structures
%A Jiri Simacek
%J Information Sciences and Technologies Bulletin of the ACM Slovakia
%D 2013
%I STU Press
%X 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).
%K hypergraphs
%K heaps
%K pointers
%K verication
%K shape analysis
%K nite tree automata
%K forest automata
%U http://acmbulletin.fiit.stuba.sk/vol5num1/simacek.pdf