Clément Hurlin
| Indirizzo | INRIA Bordeaux -- Sud-Ouest, Edificio A29 |
| 351 cours de la libération, 33405 Talence, Francia | |
| Telefono | 00 33 5 24 57 40 72 |
| sostituisci x con clement in x.hurlin@inria.fr | |
Presentazione
Faccio un post-dottorato sulla composizione di politiche di sicurezza scritte con sistemi di riscrittura. Lavoro con Hélène Kirchner.
Ho ottenuto un dottorato dell'università di Nizza - Sophia Antipolis in settembre 2009 per la mia tesi "Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic". Ho fatto la mia tesi sotto la direzione di Marieke Huisman : i due primi anni all'Inria Sophia Antipolis e il terzo e ultimo anno all'università di Twente. Prima, ho fatto l'Esial e il master dell'università di Nancy.
Ero reviewer o secondo reviewer per l'Acta Informatica giornale, BYTECODE'08, CSF'08, AMAST'08, SMT'08, BYTECODE'09, e TPHOL'09.
Prima, ero implicato nei progetti seguenti:- Verifica di programmi : Mobius
- Verifica di programmi paralleli : ParSec
- Integrazione di haRVey prover in Isabelle
- Modifica di ESC/Java2 per usare parecchi provers
Papers e relazioni
Ecco i miei papers ed una selezione di presentazioni che ho fatto. Può leggere il mio curriculum vitae in inglese o in francese. I miei interessi sono i metodi formali per la verificazione di programmi, la prova di teoremi automatizzati, e l'ingegneria del software.
Software
Ho scritto il sistema sonoro di BanKiZ (un gioco multiplayer).
Ho scritto un interactive prover per la logica lineare proposizionale: ratp.
Uso liberi software. Di fronte alla mancanza di documentazione per Metapost (un linguaggio per creare delle figure geometriche) in lingue altre dall'inglese, ho scritto una guida e la incoraggio a tradurla anche lei (sono qui le fonti): Introduzione pratica al MetaPost.
Ecco la mia lista di astuzie per Linux.
Ho (un po') completato l'eccelente riassunto Coq di Anne Pacalet: quickref.pdf, quickref.tex.
|
|
Ultima modificazione: 29 October 2009 |