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 12 septembre, 10h30

                           ---------------------
                           Jacques-Henri Jourdan
                           ---------------------

                                   INRIA

                          ========================
                          Validating LR(1) parsers
                          ========================

The CompCert verified compiler has improved the confidence we can give
to a compiler. However, some parts of the compiler still lack proofs.
Our work aims at building a verified parser for CompCert.

We present a framework for generating verified LR(1) parsers : we use a
modified version of Menhir to generate the description of an LR(1)
automaton. By proving a validator and an interpreter of such an
automaton in Coq, we are able to construct a verified parser for the
full C99 grammar.

To conclude, we will focus on two problems that appeared during this
work : the problem of non-termination of LR parsers and the context
sensitivity of the C99 grammar.