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 - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                          VENDREDI 13 octobre, 10h30

                              ------------------
                              Arthur Charguéraud
                              ------------------

                                    Inria

                 ===========================================
                   A new axiom-free implementation of CFML
                 for the verification of imperative programs
                 ===========================================

The CFML tool can be used to verify imperative OCaml programs through
interactive proofs using Coq. It is based on the generation of characteristic
formulae, which describe the semantics of the source code directly in terms of
standard logical connectives. In the original version of the CFML tool that I
designed during my PhD thesis, the characteristic formulae were produced as
axioms generated by an external program, which had to be trusted. Recently,
Armaël Guéneau showed in the context of the CakeML project in HOL that it is
possible to produce certified characteristic formulae, i.e., in an axiom-free
way. Motivated by these results, I developed a new characteristic formula
generator for CFML, this time implemented entirely within Coq. The generator,
which takes as input (the deep embedding of) a source program and computes its
characteristic formula, is proved sound once-and-for-all.  Furthermore, the
new generator for CFML adds to Armaël's work by leveraging Coq typeclasses to
inherently support specification of (deeply-embbeded) program values directly
in terms of the corresponding Coq values, a feature essential to allow for
concise and intuitive specifications. In this talk, I will show how the
generator can be defined and proved correct in just a couple hundred lines of
Coq, and show how to use it to verify examples in practice like with the prior
version of CFML.