Nazev:

  Fully Automated Shape Analysis Based on Forest Automata

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.