Lundi 28 novembre, Salle 6A92 (Sous-marin)
LIAFA, 175 rue du Chevaleret Paris 13eme

9h00 Coffee


9h15 Peter Habermehl (Liafa):  Automata-based Verification of Programs with Tree Updates

Abstract:
This paper describes an effective verification procedure for imperative programs
that handle (balanced) tree-like data structures. Since the verification problem
considered is undecidable, we appeal to a classical semi-algorithmic approach in
which the user has to provide manually the loop invariants in order to check the
validity of Hoare triples of the form $\{P\}C\{Q\}$, where $P, Q$ are the sets of
states corresponding to the pre- and post-conditions, and $C$ is the program to
be verified. We specify the sets of states (representing tree-like memory
configurations) using  a special class of tree automata named Tree Automata with
Size Constraints (TASC). The main advantage of using TASC in program
specifications is that they recognize non-regular sets of tree languages such as
the {\em AVL trees}, the  {\em red-black trees}, and in general, specifications
involving arithmetic reasoning about the lengths (depths) of various (possibly
all) paths in the tree. The class of TASC is closed under the operations of
union, intersection and complement, and moreover, the emptiness problem is
decidable, which makes it a practical verification tool. We validate our approach
considering red-black trees and the insertion procedure, for which we verify that
the output of the insertion algorithm is a {\em balanced} red-black tree, i.e.
the longest path is at most twice as long as the shortest path.

Joint work with Radu Iosif and Tomas Vojnar


10h00 Radu Iosif (Verimag): Flat Parametric Counter Automata

Abstract:
In this paper we study parametric flat counter automata and their relation with various
decidable fragments of integer arithmetic. We establish a hierarchy of flat counter automata,
by restricting the number of parameters, the number of loops and the form of the transition
relations. For each class in the hierarchy, we found a matching subtheory of integers, in the
sense that, for each automaton in the class, the reachability (emptiness) problem can be
expressed as the satisfiability of a formula in the language of a given theory, and viceversa.
Using the same arithmetic theories allowed us to also establish the relation of flat counter
automata with previous work on 2-way reversal bounded counter machines. Last, we report on an
effective procedure to answer the question whether a given 1-parametric linear Diophantine system
has a solution.

Joint work with Marius Bozga


10h45 Coffee break

11h00 Ahmed Bouajjani (Liafa): Automata-based Symbolic Reachability Analysis of Dynamic Networks of Pushdown Systems

Abstract:
We introduce abstract models for multithreaded programs based
on dynamic networks of pushdown systems. We address the problem of symbolic reachability
analysis for these models. More precisely, we consider the problem of computing effective
representations of their reachability sets using (finite-state) automata-based techniques.
We show that, while forward reachability sets are not regular in general (but context-free),
backward reachability sets starting from regular sets of configurations are always regular.
We provide algorithms for computing backward reachability sets using word/tree automata,
and show how these algorithms can be applied for flow analysis of multithreaded programs.
This is a joint work with Markus Mueller-Olm (Univ. of Dortmund) and Tayssir Touili (LIAFA, CNRS)

In a second part of the talk, we consider an extension of the models considered above with
asynchronous communication through shared variables. We show how to perform efficiently
bounded context switch reachability analysis for these (Turing powerful) models.
This is a joint work with Javier Esparza, Stephan Schwoon, and Jan Srejcek (Univ. Stuttgart)


11h45 - 13h45 Lunch

13h45 Ahmed Bouajjani (Liafa): TBA (Heap Logic Talk)

14h30 Guillaume Salagnac (Verimag):

Quelques idees sur l'analyse de pointeurs et d'echappement.
On presentera une direction de recherche qu'on explore pour mettre en oeuvre une analyse
compositionnelle avec precision parametrable pour l'analyse de pointeurs et d'echappement.
On discutera les resultats experimentaux obtenus avec un premier prototype.

15h00 Sergio Yovine (Verimag):

Etat d'avancement sur la generation de code pour la RTSJ.