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.