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 
premisses

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 
decidability.