HEAP Workshop on Verification of Programs with Dynamic Data Structures, Friday 28 May, Grenoble

9h00 - 9h30 breakfast

9h30 - 10h30 Antoine Meyer (Liafa, Paris): On Term Rewriting Systems Having a Rational Derivation

Several types of term rewriting systems can be distinguished by the way their
rules overlap. In particular, we define the classes of prefix, suffix,
bottom-up and top-down systems, which generalize similar classes on words.
Our aim is to study the derivation relation of such systems (i.e. the
reflexive and transitive closure of their rewriting relation) and, if
possible, to provide a finite mechanism characterizing it. Using a notion of
rational relations based on finite graph grammars, we show that the derivation
of any bottom-up, top-down or suffix system is rational, while it can be non
recursive for prefix systems.

10h30 - 11h30 Dino DiStefano (Queen Mary, London): Who is Pointing When to Whom? On the automated verification of linked list structures

(joint work with Joost-Pieter Katoen and Arend Rensink)

This talk introduces an extension of linear temporal logic that allows to
express properties about systems that are composed of entities (like objects)
that can refer to each other via linearly linked pointers. Our logic is
focused on specifying properties about the dynamic evolution (such as creation,
adaptation, and removal) of such pointer structures. The semantics is based on
automata on infinite words, extended with appropriate means to model evolving
pointer (i.e., heap) structures in an abstract manner. A tableau-based
model-checking algorithm is proposed to automatically verify these automata
against formulae in our logic.

11h30 - 12h30 Josh Berdine (Queen Mary, London): A Decidable Fragment of Separation Logic

(joint with Cristiano Calcagno and Peter O'Hearn)

A small fragment of separation logic and a procedure for deciding validity of
entailments between formulae is described. The fragment includes only a single
inductive predicate, describing segments of linked lists (essentially
reachability), and restricts formulae to a special form whose main
characteristic is the inability to express ``unspecified sharing''. That is,
general separation logic formulae are sometimes modeled by heaps (worlds)
where some parts of a heap model multiple subformulae. The fragment rules out
such formulae, roughly leaving only those whose models can be split into
separate pieces for each subformula. While admittedly very small, the
observation that the specifications of many list-manipulating pointer programs
fit into this fragment motivated our investigation. The key to decidability is
the inability of formulae in the fragment to distinguish between different
models (of the inductive case) of the list segment predicate. This, together
with separation logic's finite model property, allows ignoring all but a
couple heaps in the search for a countermodel. This can also be seen as
abstracting arbitrarily-many heaps to two. Proof theoretically, this
manifests as a rule which infers an inductive property from non-inductive

12h30 - 14h00 lunch

14h00 - 15h00 Radu Iosif (Verimag, Grenoble): Logics of Aliasing - strengths and weaknesses

(joint work with Marius Bozga and Yassine Lakhnech)

In this talk I will survey three logics for specification of heap topologies.
The first one, called weak Alias Logic (wAL) can describe the shapes of most
recursively defined data structures (lists, trees, etc.) has a complete
weakest precondition calculus but is undecidable. The second one , called
propositional Alias Logic (pAL) is  a decidable subset of wAL, closed
under weakest precondition which does not allow to talk about unbounded heap
structures (yet bounded structures can be characterized up to isomorphism).
The third logic, called counting Alias Logic (kAL) is introduced in order to
bridge the expressivity gap between the two first. Even though the general
satisfiability problem is undecidable, the logic shows interesting connections
with the arithmetic theories of natural numbers, for which a large number of
decidability results have been given (Presburger arithmetic, Groebner bases,
etc). The three logics presented here can be seen as elements of a framework
which attempts to reconcile the naturally oposite goals of expressiveness and