Réunion du 6 novembre 2006

Programme de la réunion

10h00	Café
10h15	Etienne Lozes(LSV) Une logique temporelle pour les programmes à pointeurs (slides)
11h15	Radu Iosif(VERIMAG) Applications of first-order Integer Arithmetic to the Verification of Programs with Lists (slides)
12h15	Déjeuner
13h30	Peter Habermehl(LIAFA) Abstract Tree Regular Model Checking of Complex Dynamic Data Structures (slides)
14h30	Discussion sur la deuxième étude de cas fournie par EDF R & D
15h15	Café
15h30	Discussion générale (Avancement première étude de cas, définition du modèle, organisation page WEB, pages internes,etc.)

Abstract des différents exposés

Une logique temporelle pour les programmes à pointeurs (E. Lozes)

Je présenterai un aperçu de l'utilisation récente des logiques temporelles dans la vérification de programmes à pointeurs, puis je présenterai le travail mené actuellement avec Rémi Brochenin et Stéphane Demri sur la définition d'une extension temporelle de la logique de séparation.

Applications of first-order Integer Arithmetic to the Verification of Programs with Lists (R. Iosif)

The arithmetic of natural numbers with addition and divisibility has been shown undecidable as a consequence of the fact that multiplication of natural numbers can be interpreted into this theory, as shown by J. Robinson (1949). The most important decidable subsets of the arithmetic of addition and divisibility are the arithmetic of addition, proved by M. Presburger (1929), and the purely existential subset, proved independently by A. Beltyukov and L. Lipshitz (1976). In the first part of the talk, we will investigate the decidability of a new subset of the arithmetic with addition and divisibility, consisting of formulae with quantifier prefix in the language $Q^* \{\exists, \forall\}^*, Q \in \{\exists, \forall\}$, where the first Q-quantified variables are the variables occurring to the left of the divisibility predicate. The advantage of this subset is that it allows a limited form of quantifier alternation. In the second part of the talk, we will analyze the complexity of checking safety and termination properties, for a very simple, yet non-trivial, class of programs with singly-linked list data structures. Since, in general, programs with lists are known to have the power of Turing machines, we restrict the control structure, by forbidding nested loops and destructive updates. Surprisingly, even with these simplifying conditions, the class of programs working on heaps with more than one cycle has undecidable safety and termination problems, whereas decidability can be established when the input heaps may have at most one loop. The proofs for both the undecidability and the decidability results rely on the number-theoretic results presented previously. The talk extends some results presented at FOSSACS 2005 and is joint work with Marius Bozga (Verimag, F).

Abstract Tree Regular Model Checking of Complex Dynamic Data Structures (P. Habermehl)

We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case studies.