Abstract: Verified programming environments are invading general-purpose software development:
F*, Liquid Haskell, and to different extends Frama-C, CompCertX, or Cogent, are all open-source
projects offering one to combine the programming of an application with the proof of its correctness,
up to logical requirements specified as types, monads and effects, simply by reifying the program as
its proof.
Verified programming combines the specification, abstraction and proof capabilities using the notion
of refinement type {v: Int | v>0} to, e.g., denote the values v of type Int that are strictly positive, and
*assume* a function to be called with such numbers and give the opposite *guarantee* on its result:
x:{v:Int | v>0} -> {w: Int | w<0}, ergo for arrays, pointers, streams, threads, exceptions, the TLS
protocol.
The power of an environment like F* (and some of the others) is that one can write the complete
specification of a micro-controller, prove it against the TCB of some hardware platform (e.g. an arduino)
and generate a verified and readable 800-locs of C code that directly boots on it.
The aim of this talk is to give a gentle introduction to the notion of refinement type, at the core of these
general-purpose environment, and to demonstrate the potential benefits of such tools for the verified
(safe and secure) design of embedded systems (CPS) which our team in currently starting to explore in
several directions.
Bio: Jean-Pierre Talpin is senior scientist with INRIA and scientific leader of INRIA project TEA.
Graduated in Applied Mathematics, he received a Master in Theoretical Computer Science from
University Paris VI and did his Ph.D. Thesis at Ecole des Mines de Paris. He received the 2004 ACM
Award for the most influential POPL paper, with Mads Tofte, and the 2012 ACM/IEEE LICS Test of
Time Award, with Pierre Jouvelot. http://www.irisa.fr/prive/talpin.
