I am doing a PhD thesis in the Everest research team.
I am supervised by
My PhD thesis is about formal validation of system components in Java. (You can find a description in french here)
My interests include tools for static verification, especially support
for interactive verification (Coq), as well
as Java, JML, refinement and aspect oriented programming.
I wrote a multi-prover editor within Eclipse: Prover Editor, To download it the update site can be found here.
And I also worked on the support of interactive verification inside of Jack.
(for more details about my publications go there)
(written in collaboration with J. Kiniry)
JACK: a tool for validation of security and behaviour of Java applications (presented at FMCO06) pdf
(written in collaboration with G. Barthe, L. Burdy, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova and A. Requet)
Adding native specifications to JML (presented at FTfJP06) ps slides
Vérification d'un composant Java: le vérificateur de bytecode (Master's Thesis) ps slides
Mobius Direct VCGen (draft) pdf slides
Taking into account Java's Security Manager for static verification (draft) pdf slides
Adding native specifications to JML (draft, a longer version) ps
Playing with Coq in Jack (Gemplus) slides
Different ways of annotating and proving a quicksort in Jack (Geccoo) slides
Different ways of annotating and proving a quicksort in Jack (Séminaire lemme/everest) slides
Playing with Coq in Jack and ESC/Java2 (Spops) slides
Vérification d'un composant système Java (présoutenance) ps slides
Vérification d'un composant Java: le vérificateur de bytecode (Geccoo) slides
Modular specification of frame properties in JML (Informal meetings over an article)
Desugaring JML method specifications (Informal meetings over an article) slides
k (a translator from a language just like
Its home page is: http://www.nongnu.org/specialk/
My library to do some slides with latex.
Jack's CoqPlugin Ml tactics version 0.2
A library for the latex' listings package to pretty print Coq source (written by Guillaume Dufay) : lstlangcoq.sty
-- last update: 03 - 19 - 08
|Made with emacs
|Valid HTML 4.01 Strict and Valid CSS!