Julien Charles
|
|
|
|
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.
(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
Modular specification of frame properties in JML (Informal meetings over an article)
slides
Desugaring JML method specifications (Informal meetings over an article)
slides
special
k (a translator from a language just like
Erlang
to
Scheme)
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
Everest
Mobius
Jack
ESC/Java2
Geccoo
Spops
-- last update: 03 - 19 - 08
Made with emacs 
|
Valid HTML 4.01 Strict and Valid CSS! |
|---|