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

***  Mercredi 10 Janvier 2007, 14h00-15h30 **************************
*** UNSUAL DATE !!!
*** salle INFO4 !!!

Chin Wei Ngan  (National University of Singapore)

Automatic Verification via Separation Logic

Abstract :

Despite their popularity and importance, pointer-based programs remain a
major challenge for program verification.  In this talk, we propose an
automated verification system that is concise, precise and expressive for
ensuring the safety of pointer-based programs.  Our approach uses
user-definable shape predicates to allow programmers to describe a wide
range of data structures with their associated size properties.  To support
automatic verification, we design a new entailment checking procedure that
can handle well-founded inductive predicates using unfold/fold reasoning.
To improve expressivity, we support a non-deterministic set of states for
proof search, intersection types for methods and coercion rules for related
shape predicates.  We have proven the soundness and termination of our
verification system, and have built a prototype system.


*** Jeudi 11 janvier 2007, 10h30-12h00 *********************************
*** UNSUAL DATE & TIME !!!
*** salle INFO 4 !!!

Sumit Gulwani (Microsoft Research, Redmond)

Program Verification using Probabilistic Techniques

Abstract: 

Probabilistic algorithms have played a significant role in several    
areas of computer science. Such algorithms are usually more precise, efficient,
and even simpler than their deterministic counterparts. In this talk, I will   
talk about two sampling based probabilistic techniques for discovering and     
proving program invariants.
                                                                                
One of these techniques, called random interpretation, can be seen as combining 
the complementary strengths of abstract interpretation and random testing. The 
key idea of this technique is to compute and manipulate program invariants     
efficiently by representing them by a small random sample of the set of program
states that they represent (as opposed to manipulating program invariants      
symbolically).                                                                 
                                                                                
The other technique can be seen as combining the complementary strengths of     
forward and backward program analysis. This technique finds correctness proofs 
of a pre/post condition pair by providing an invariant at each program point   
that can be locally verified. This is done by first initializing the (guesses  
for the) invariants at all program points to anything, and then iteratively    
selecting a random program point and updating its invariant randomly to make it
more locally consistent with respect to the invariants at the neighboring      
points.                                                                        

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