Detail publikačního výsledku

Fully Automated Shape Analysis Based on Forest Automata

HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.

Originální název

Fully Automated Shape Analysis Based on Forest Automata

Anglický název

Fully Automated Shape Analysis Based on Forest Automata

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

forest automata, shape analysis, dynamic linked data structures, tree automata, abstraction

Klíčová slova v angličtině

forest automata, shape analysis, dynamic linked data structures, tree automata, abstraction

Autoři

HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.

Rok RIV

2014

Vydáno

15.07.2013

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-642-39798-1

Kniha

Proceedings of CAV'13

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

8044

Stát

Spolková republika Německo

Strany od

740

Strany do

755

Strany počet

16

BibTex

@inproceedings{BUT103488,
  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",
  booktitle="Proceedings of CAV'13",
  year="2013",
  journal="Lecture Notes in Computer Science",
  number="8044",
  pages="740--755",
  publisher="Springer Verlag",
  address="Heidelberg",
  isbn="978-3-642-39798-1",
  issn="0302-9743"
}