moi

Julien Charles

Organization: INRIA
Research Unit: Sophia Antipolis
Project: Everest
Phone: (+33/0) 4 92 38 75 65
Fax: (+33/0) 4 92 38 50 29
E-mail: Julien.Charles@inria.fr




I am doing a PhD thesis in the Everest research team. I am supervised by Benjamin Grégoire.
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.


Written things about my work:

(for more details about my publications go there)

A lightweight theorem prover interface for Eclipse (will be presented at UITP08) pdf
     (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

Written things about the work of others:

Modular specification of frame properties in JML (Informal meetings over an article) slides
Desugaring JML method specifications (Informal meetings over an article) slides

My Master 1's project :

special k (a translator from a language just like Erlang to Scheme)
Its home page is: http://www.nongnu.org/specialk/

Old useful things :

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

Some links:

Everest
Mobius
Jack
ESC/Java2

Geccoo
Spops



--
last update: 03 - 19 - 08
Made with emacs a dog Valid HTML 4.01 Strict and Valid CSS!