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.