Ondrej Lengal

"Fully Automated Shape Analysis Based on Forest Automata"

1 hour

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.

Bio:

  Ondrej Lengal is a Ph.D. student at Brno University of Technology,

  Czech Republic, under the supervision of Tomas Vojnar. His main

  interests are shape analysis and automata theory