To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 08/02/10 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                           Lundi 8 février, 10h30

                              ----------------
                              Virgile Prevosto
                              ----------------

                                    CEA

        ===========================================================
        Specification and Proof of C Programs with Frama-C and ACSL
        ===========================================================

Frama-C is a framework dedicated to the analysis of C programs. It
features a very modular design, in which various kinds of analysis
are built as plugins on top of a kernel which takes care of
maintaining the internal state of the whole analyzer. At the core of
this design lies ACSL, the ANSI/ISO C Specification Language, which
allows the user to express the intended properties of the program, but
also the plugins to exchange some information through ACSL assertions.
In this talk, we will briefly present the overall Frama-C architecture.
Then, we will show how ACSL can be used to specify the behavior of C
functions and how to prove with Frama-C that the corresponding
implementations are correct with respect to these specifications.