Skip to main content
Department of Information Technology

Fully Automated Shape Analysis Based on Forest Automata


Ondrej Lengal, Brno University of Technology, Czech

Date and Time

Tuesday, June 11th, 2014 at 11:00.


Polacksbacken, room 4308


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. 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.

Updated  2014-06-10 16:41:23 by Mohamed Faouzi Atig.