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.