SKLCS Seminar
Title: Fully Automated Shape Analysis Based on Forest Automata
Speaker: Ondrej Lengal (Institute of Information Science, Academia Sinica, Taiwan)
Time: 15:00, December 16th (Wednesday), 2015.
Venue: Seminar Room (334), Level 3, Building 5, Institute of Software,
Chinese Academy of Sciences.
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.
Biography:
Ondrej Lengal received his master's and PhD degree at Brno University
of Technology, Czech Republic, under the supervision of Tomas Vojnar.
His main research interests are shape analysis and automata theory,
with applications in decision procedures of logics. He is currently
a postdoc at Institute of Information Science, Academia Sinica, Taiwan.
--------------------
ALL ARE WELCOME!
