*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h00                     *
*                        Salle W (Toits du DI)                      *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


***  Vendredi 19 Mars 2010, 14h00-15h00 ************************

A Certified Denotational Abstract Interpreter

David Pichardie, INRIA Rennes

Re'sume'/ Abstract:

Abstract Interpretation proposes advanced techniques for static
analysis of programs that raise specific challenges for
machine-checked soundness proofs. Most classical dataflow analysis
techniques iterate operators on lattices without infinite ascending
chains. In contrast, abstract intepreters are looking for fixpoints
in infinite lattices where widening and narrowing are used for
accelerating the convergence. Smart iteration strategies are crucial
when using such accelerating operators because they directly impact
the precision of the analysis diagnostic. In this work, we show
how we manage to program and prove correct in Coq an abstract
interpreter that uses iteration strategies based on program syntax.
A key component of the formalisation is the introduction of an
intermediate semantics based on a generic least-fixpoint operator
on complete lattices that allows us to decompose the soundness proof in an
elegant manner.



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