Mardi 1 mars, Salle 6A92 (Sous-marin)
LIAFA, 175 rue du Chevaleret Paris 13eme

9h00 Coffee

9h15 Tayssir Touili (LIAFA) :
     An Expressive Framework for State/Event Systems



Abstract:
Specification languages for concurrent software systems need to
combine practical algorithmic efficiency with high expressive power
and the ability to reason about both states and events. We address
this question by defining a new branching-time temporal logic
 which integrates both state-based and action-based
properties. This logic  is universal, i.e., preserved by the simulation
relation, and thus amenable to counterexample-guided abstraction
refinement.  We provide a model-checking algorithm for this logic, and
describe a compositional abstraction-refinement loop which exploits
the natural decomposition of the concurrent system; the abstraction
and refinement steps are performed over each component separately, and
only the model checking step requires an explicit composition of the
abstracted components.  For experimental evaluation, we have
integrated the presented algorithms in the software verification tool
MAGIC, and determined a previously unknown race condition error in a
piece of an industrial robot control software.

10h00 Pause

10h15 Peter Habermehl (LIAFA):
      Verifying Programs with 1-Selector-Linked Structures in Regular Model Checking

Abstract:
We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory aresystematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduce new techniques for the computation of abstractions of the set of reachable configurations and to refine these abstractions if spurious counterexamples are detected. Finally, we present experimental results showing the applicability of the approach and its efficiency.
acceleration problem for integer counter automata.

11h00 Pause

11h15 Radu Iosif (VERIMAG):
      "Quantitative Verification of Programs with Lists"

In this work we study imperative programs that handle list objects, performing unrestricted selector updating operations. For this class of programs, we address the problem of {\em quantitative verification}, by reasoning about arithmetic relations between the lengths of certain lists. We first show undecidability of the general problem, by reduction from the reachability problem for two-counter machines. Second, we introduce a decidable property specification logic and we study the complexity of the decision problem. Finally, we propose a semi-algorithmic method for the verification of Hoare-Floyd style properties of programs with lists. Using this method, we can reduce the invariant computation problem for a program with lists to an acceleration problem for integer counter automata.

12h00 Pause

13h30 Julien D'Orso (LIAFA):
      Simulation-Based Iteration of Tree Transducers

Abstract:
Regular model checking is the name of a family of techniques for
analyzing infinite-state systems in which states are represented by
words, sets of states by finite automata, and transitions by
finite-state transducers. The central problem is to
compute the transitive closure of a transducer. A main obstacle
is that the set of reachable states is in general not regular.
Recently, regular model checking has
been extended to systems with tree-like architectures.
In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states which are related according to a pre-defined equivalence relation. The equivalence is induced by a {\it downward} and an {\it upward} simulation relation which can be efficiently computed. Our technique can also be used to compute the
set of reachable states without computing the transitive closure. We
have implemented and applied our technique to several protocols.

14h15 Guillaume Salagnac (VERIMAG):
     "Fast escape analysis for region-based memory management"

Abstract: We present an algorithm for escape analysis inspired by, but
  more precise than, the one proposed by Gay and Steensgaard. The
  primary purpose of our algorithm is to produce useful information to
  allocate objects using a region-based memory manager. The algorithm
  combines intraprocedural variable-based and interprocedural points-to
  analyses. This is a work in progress towards achieving an
  application-oriented trade-off between precision and scalability. We
  illustrate the algorithm on several typical programming patterns, and
  show experimental results of a first prototype on a few benchmarks.

15h00 Discussion