Not registered as user yet
Name: Jean-Christophe Filliatre
Bio: I did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Coq. Right after my PhD, in fall 1999, I redesigned the architecture of Coq, to isolate a kernel ; this is briefly described in this paper. Then I left for a post-doc at SRI, in the PVS team, where I started the development of the ICS decision procedure. When I returned to France, I started in 2001 the development of a tool for program verification called Why, used for the proof of C programs (in the Caduceus tool, now subsumed by Frama-C) and for the proof of Java programs in the Krakatoa tool. In 2010, the Why tool became Why3.
Affiliation: CNRS, Paris, France
Personal website: https://www.lri.fr/~filliatr/#
ECOOP 2015 Activities
View general profile