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

Registered user since Sat 18 Jul 2020

Name:Jean-Christophe Filliatre

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


Show activities from other conferences

ECOOP 2015-profile
View general profile