Publication Details
Fully Automated Shape Analysis Based on Forest Automata
Lengál Ondřej, Ing., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
forest automata, shape analysis, dynamic linked data structures, tree automata,
abstraction
Forest automata (FA) have recently been proposed as a tool for shape analysis of
complex heap structures. FA encode sets of tree decompositions of heap graphs in
the form of tuples of tree automata. In order to allow for representing complex
heap graphs, the notion of FA allowed one to provide user-defined FA (called
boxes) that encode repetitive graph patterns of shape graphs to be used as
alphabet symbols of other, higher-level FA. In this paper, we propose a novel
technique of automatically learning the FA to be used as boxes that avoids the
need of providing them manually. Further, we propose a significant improvement of
the automata abstraction used in the analysis. The result is an efficient,
fully-automated analysis that can handle even as complex data structures as skip
lists, with the performance comparable to state-of-the-art fully-automated tools
based on separation logic, which, however, specialise in dealing with linked
lists only.
@techreport{BUT192914,
author="Lukáš {Holík} and Ondřej {Lengál} and Adam {Rogalewicz} and Jiří {Šimáček} and Tomáš {Vojnar}",
title="Fully Automated Shape Analysis Based on Forest Automata",
year="2013",
publisher="Faculty of Information Technology BUT",
address="FIT-TR-2013-01, Brno",
pages="1--25",
url="http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2013-01.pdf"
}