Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 2, bâtiment C

                           Lundi 8 novembre, 10h30

                                -------------
                                Mário Pereira
                                -------------

                   NOVA-LINCS, Universidade Nova de Lisboa

              =================================================
              Cameleer: a Deductive Verification Tool for OCaml
              =================================================

OCaml is particularly well-fitted for formal verification. On one
hand, it is a multi-paradigm language with well-defined semantics,
allowing one to write clean, concise, type-safe, and efficient code.
On the other hand, it is the language of choice for the implementation
of sensible software, e.g., industrial compilers, proof assistants,
and automated solvers. Yet, with the notable exception of some
interactive tools, formal verification has been seldom applied to
OCaml-written programs. In this talk, we present the ongoing project
Cameleer, aiming for the development of a deductive verification tool
for OCaml, with a clear focus on proof automation. We leverage on the
recently proposed GOSPEL, Generic OCaml SPEcification Language, to
attach rigorous, yet readable, behavioral specification to OCaml code.
The specified program is fed to our toolchain, which translates it
into an equivalent program in WhyML, the programming and specification
language of the Why3 verification framework. Finally, Why3 is used to
compute verification conditions, which can be discharged by
off-the-shelf SMT solvers. We will present some successful case
studies conducted with the Cameleer tool, namely the verification of
modules issued from widely used OCaml libraries.