|
Evènement pour le groupe Modélisation et Verification
Date | 2012-01-26 11:30-12:30 |
Titre | Forest Automata for Verification of Heap Manipulation |
Résumé | We consider verification of programs manipulating
dynamic linked data structures such as various forms of singly and doubly-linked
lists or trees. We consider important properties for this kind of systems like
no null-pointer dereferences, absence of garbage, shape properties, etc. We
develop a verification method based on a novel use of tree automata to represent
heap configurations. A heap is split into several ``separated'' parts such that
each of them can be represented by a tree automaton. The automata can refer to
each other allowing the different parts of the heaps to mutually refer to their
boundaries. Moreover, we allow for a hierarchical representation of heaps by
allowing alphabets of the tree automata to contain other, nested tree automata.
Program instructions can be easily encoded as operations on our representation
structure. This allows verification of programs based on a symbolic state-space
exploration together with refinable abstraction within the so-called abstract
regular tree model checking. A motivation for the approach is to combine
advantages of automata-based approaches (higher generality and flexibility of
the abstraction) with some advantages of separation-logic-based approaches
(efficiency). We have implemented our approach and tested it successfully on
multiple non-trivial case studies.
(joint work with Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar) |
Lieu | 076 |
Orateur | Peter Habermehl |
Email | Peter.Habermehl@liafa.jussieu.fr |
Url | LIAFA, Paris |
Aucun document lié à cet événement. RetourRetour à l'index
| |