*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*   ENS, Equipe-projet INRIA "Abstraction" commune avec ENS & CNRS  *
*                                                                   *
*                        Vendredi, 14h00--16h00                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

***  Vendredi 06 Mars 2009, 14h00-15h00 *****************************

From Monothread to Multithread

Jean-Loup Carre', LSV ENS-Cachan

Re'sume'/ Abstract:

A great variety of static analyses that compute safety properties of
monothreaded programs have now been developed.  I present a systematic
method to extend a class of such static analyses, so that they handle
programs with multiple POSIX-style threads.  Starting from a pragmatic
operational semantics, we build a denotational semantics that expresses
reasoning Ì  la assume-guarantee.  The final algorithm is then derived by
abstract interpretation.  It analyses each thread in turn, propagating
interferences between threads, in addition to other semantic information.
The combinatorial explosion, ensued from the explicit consideration of all
interleavings, is thus avoided.  Prototype tools have been implemented,
demonstrating the practicality of the approach.


***  Vendredi  20 Mars 2009, 14h00-15h00 *****************************

TVLA: A system for inferring quantified invariants

Mooly Sagiv, School of Computer Science, Tel-Aviv University

Re'sume'/ Abstract:

The TVLA system was originally designed as a system for inferring shape
properties. In this talk, I will present both the traditional view and the
also I will show that the TVLA abstractions amounts to representing
invariants in a limited form. This allows TVLA to prove properties which are
not usually viewed as shape properties and also sheds some light on the
limitations of TVLA and in particular the state space explosion. Moreover, I
will present TVLA operations as effective heuristics for reasoning about
quantified invariants which includes: materialization, finite differencing,
Kleene evaluation, and consequence finding This is a joint work with Tal
Lev-Ami (Tel Aviv University), Roman Manevich (UCLA), G. Ramalingam (MSR),
Tom Reps (University of Wisconsin), Reinhard Wilhelm (Sarrland University),
and Greta Yorsh (IBM Research)


***  Vendredi  27 Mars 2009, 14h00-15h00 *****************************

Automated rely-guarantee reasoning for heap-manipulating programs

Viktor Vafeiadis, Microsoft Research Cambridge 

Re'sume'/ Abstract:

I shall present an automatic thread-modular procedure for verifying
concurrent heap-manipulating programs.  This procedure computes a set of
RGSep actions, which overapproximate the interference that each thread
causes to its concurrent environment.  This allows us to verify safety and
liveness properties of a collection of practical concurrent algorithms.



*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************