ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague 1, Czech Republic
Jean-Christophe Filliatre

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.

Country: France

Affiliation: CNRS, Paris, France

Personal website:

ECOOP 2015 Activities

ECOOP 2015-profile
View general profile