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)
                                   En ligne

                           Lundi 7 décembre, 10h30

                              ------------------
                              Raphaël Rieu-Helft
                              ------------------

                   Laboratoire de Recherche en Informatique

         ===========================================================
         Verification of efficient C arithmetic algorithms with Why3
         ===========================================================

Arbitrary-precision integer arithmetic algorithms are used in contexts where
both their performance and their correctness are critical, such as
cryptographic software or computer algebra systems. GMP is a very widely-used
arbitrary-precision integer arithmetic library. It features state-of-the-art
algorithms that are intricate enough that their formal verification is both
justified and difficult. This work tackles the formal verification of the
functional correctness of a large fragment of GMP using the Why3 deductive
verification platform.

We have developed models of the memory management and datatypes of the C
language in WhyML, Why3's functional programming and specification language.
This allowed us to reimplement GMP's algorithms in WhyML and verify them. We
have also extended Why3's extraction mechanism so that WhyML programs can be
compiled to idiomatic C code, where only OCaml used to be supported.

The result of this extraction is a verified C library called WhyMP. It
implements many algorithms from GMP, with almost all of the optimization
tricks preserved. WhyMP is compatible with GMP and performance-competitive
with the assembly-free version.