Clément Hurlin

Physical address	INRIA Bordeaux -- Sud-Ouest, Building A29
	351 cours de la libération, 33405 Talence, France
Phone	00 33 5 24 57 40 72
Email	replace x by clement in x.hurlin@inria.fr

Presentation

I'm a postdoc working on the composition of rule-based security policies under the guidance of Hélène Kirchner.

I obtained a PhD from the university of Nice - Sophia Antipolis in September 2009 for my thesis entitled "Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic". The work on my thesis took place in between September 2006 and September 2009 with Marieke Huisman as my advisor. I spent the first two years of my PhD at Inria Sophia Antipolis and spent the final third year at Twente's university. Previously, I graduated from the Esial and the university of Nancy.

I have been a reviewer or second reviewer for the Acta Informatica journal, BYTECODE'08, CSF'08, AMAST'08, SMT'08, BYTECODE'09, and TPHOL'09.

In the past, I worked in the following projects:

Security of programs: Mobius
Security of parallel programs: ParSec
Integrating the haRVey prover within Isabelle
Modifying ESC/Java2 to handle multiple provers

Papers and talks

Here are my papers and a selection of talks I have given. You can read my curriculum vitae in english or in french. My interests principally lie in formal methods for program verification, theorem proving, and software engineering.

Software

I modified (a bit) Anne Pacalet's excellent Coq quick reference/cheat sheet: quickref.pdf, quickref.tex.

I've written an interactive prover called ratp for a variant of propositional linear logic.

I keep a list of linux tricks.

I use free software. Because of the lack of documentation for MetaPost (a language to generate geometrical figures), I wrote a tutorial and I encourage you to translate it as well (here are the sources): Practical introduction to MetaPost.

I've written the sound system for BanKiZ (a free multiplayer game written in C++).

Last modification: October 26, 2009