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

                           Lundi 14 octobre, 10h30

                              ------------------
                              Jonathan Protzenko
                              ------------------

                              Microsoft Research

                =============================================
                The EverCrypt verified cryptographic provider
                =============================================

EverCrypt is a comprehensive collection of verified, high-performance
cryptographic functionalities available via a carefully designed API. The API
provably supports agility (choosing between multiple algorithms for the same
functionality) and multiplexing (choosing between multiple implementations of
the same algorithm).

I will first give a high-level overview: supported algorithms, performance,
general architecture of the library. I will then switch to a more PL
perspective, showing how the judicious use of meta-programming allows us to
avoid a lot of effort. I will also dwell on our style of stateful abstract
invariants stated against abstract specifications.