Publication Details

Fully Automated Shape Analysis Based on Forest Automata

HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.
Czech title
Plně automatizovaná analýza haldy programů založená na lesních automatech
Type
conference paper
Language
english
Authors
Keywords
forest automata, shape analysis, dynamic linked data structures, tree automata, abstraction
Abstract

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.

Published
2013
Pages
740-755
Journal
Lecture Notes in Computer Science, no. 8044, ISSN 0302-9743
Proceedings
Proceedings of CAV'13
Conference
25th International Conference on Computer Aided Verification -- CAV 2013, Saint Petersburg, RU
ISBN
978-3-642-39798-1
Publisher
Springer Verlag
Place
Heidelberg, DE
BibTeX
@INPROCEEDINGS{FITPUB10322,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Adam Rogalewicz and Ji\v{r}\'{i} \v{S}im\'{a}\v{c}ek and Tom\'{a}\v{s} Vojnar",
   title = "Fully Automated Shape Analysis Based on Forest Automata",
   pages = "740--755",
   booktitle = "Proceedings of CAV'13",
   journal = "Lecture Notes in Computer Science",
   number = 8044,
   year = 2013,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-39798-1",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10322"
}
Back to top