[12-16]Fully Automated Shape Analysis Based on Forest Automata

文章来源:  |  发布时间:2015-12-08  |  【打印】 【关闭

  
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!