*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h00                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


***  Vendredi 26 septembre 2008, 14h00-15h00 ************************

Thread-modular heap analysis

Alexey Gotsman, University of Cambridge

Re'sume'/ Abstract:

We present a static analysis for verifying memory-safety and data race
freedom properties of multithreaded programs that avoids the explicit
enumeration of execution-interleavings. Our analysis is inspired by
concurrent separation logic and is based on automatic inference of a
resource invariant associated with each lock that describes the part of
the heap protected by the lock. This allows us to use a sequential
static analysis on each thread. Experiments with applying our prototype
implementation to concurrent heap-manipulating code from Windows device
drivers show that the analysis is precise and scalable. This is joint
work with Josh Berdine, Byron Cook and Mooly Sagiv.

***  Vendredi 26 septembre 2008, 15h15-16h15 ************************

CTL as an Intermediate Language

Neil D. Jones and Rene Rydhof Hansen, University of Copenhagen

Re'sume'/ Abstract:

The Coccinelle system is a program transformer used to automate and 
document collateral evolutions in Linux device drivers. Semantics are 
developed for the its underlying semantic patch language (SmPL). A 
richer and more effcient version is defined, implemented by
compiling to the temporal logic CTL-V as an intermediate language.

This talk describes a semantics example, a correctness proof, and
sketches a model checker. Two semantics are developed:
a traditional continuation semantics, and an
alternative that uses a temporal logic as intermediate compiling language.
The first is denotational - in essence an executable higher-order functional
program, but inefficient and limited to straight-line source
programs. Alternately, compiling into CTL-V ameliorates both
problems. The compilation is proven correct and a model check algorithm is
outlined.

CTL-V is CTL extended with existentially quantified variables ranging
over source code parameters and program points. Quantification is defined 
using the staging concept from partial evaluation.

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