¡@
"Fully Automated Shape Analysis Based on Forest Automata"
1 hour
Abstract:
Forest automata (FAs) have recently been proposed as a tool for shape
analysis of complex heap structures [1]. FAs encode sets of tree
decompositions of heap graphs in the form of tuples of tree automata.
In order to allow representing complex heap graphs, the notion of FAs
allowed one to provide user-defined FAs (called boxes) that encode
repetitive graph patterns of shape graphs to be used as alphabet
symbols of other, higher-level FAs. Later, we proposed a novel
technique of automatically learning the FAs to be used as boxes that
avoids the need of providing them manually [2]. The result was an
efficient, fully-automated analysis that could handle even as complex
data structures as skip lists. In the most recent contribution [3], we
extended the framework with constraints between data elements
of nodes in the heaps represented by FAs, modifying the abstract
interpretation used, to allow us verify programs depending on ordering
relations among data values. We evaluated our approach on programs
manipulating different flavours of lists (singly/doubly linked,
circular, nested, ...), trees, skip lists, and their combinations.
The experiments show that our approach is not only fully automated,
rather general, but also quite efficient.
[1] P. Habermehl, L. Holik, J. Simacek, A. Rogalewicz, and T. Vojnar.
Forest Automata for Verification of Heap Manipulation. In Proc. of
CAV'11.
[2] L. Holik, O. Lengal, J. Simacek, A. Rogalewicz, and T. Vojnar.
Fully Automated Shape Analysis Based on Forest Automata. In Proc.
of CAV'13.
[3] P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T.
Vojnar. Verification of Heap Manipulating Programs with Ordered
Data by Extended Forest Automata. In Proc. of ATVA'13.
Bio:
Ondrej Lengal is a Ph.D. student at Brno University of Technology,
Czech Republic, under the supervision of Tomas Vojnar. His main
interests are shape analysis and automata theory