Sébastien Bardin's Homepage

Sébastien BARDIN

Chercheur en Informatique

Formation
Docteur en Informatique de l'ENS Cachan, 2005
Ingénieur de l'ENSIIE, 2002

Poste actuel
Chercheur,
Laboratoire de Sûreté Logicielle,
Commissariat à l'Energie Atomique (CEA),
Paris-Région, France

Contact
Mél. : sebastien.bardin(at)cea.fr
Tél. : +33 (0)1 69 08 54 16
Adr. : CEA Saclay, Bâtiment 528, Pièce 135
91191 Gif sur Yvettes, France

J'ai effectué ma thèse de doctorat au Laboratoire Spécification et Vérification (ENS Cachan), où mes travaux ont portés sur la vérification automatique de systèmes "infinis" via des techniques de représentations symboliques et d'accélération. Je me suis plus particulièrement intéressé aux systèmes manipulant des compteurs et de la mémoire dynamique. J'ai notamment participé à la réalisation du logiciel FAST (model-checking de systèmes à compteurs). J'ai ensuite rejoint en 2006 le Laboratoire de Sûreté Logicielle du CEA Saclay. Je travaille maintenant sur la vérification de codes binaires exécutables, en utilisant des combinaisons de techniques symboliques et concrètes.

mon ancienne page de l'ENS Cachan

Thèmes de recherche

Thème général : validation et vérification, génie logiciel, méthodes formelles, vérification de programmes, vérification de modèles
Sous-domaine : (software) model checking, test automatique, exécution concolique, analyse statique
Domaines d'applications possibles : systèmes embarqués, systèmes critiques, sécurité informatique, productivité logicielle

Vérification de codes binaires

Compréhension d'un exécutable et génération automatique de tests
Exécution concolique
Prototype OSMOSE [génération automatique de tests sur du code binaire] (slides)
Prototype CFGBuilder [reconstruction sûre de CFG] (slides)
le modèle des DBA pour l'analyse de code binaire et le DBA Toolkit (slides)

Model checking de systèmes infinis (passé)

Systèmes à compteurs, systèmes à mémoire dynamique, systèmes hétérogènes
Représentations symboliques et Accélération

Logiciels FAST et FASTeR [model checking de systèmes à compteurs]

News

06/01/2013 - 11/01/2013: Dagstuhl seminar "Symbolic Methods in Testing" (slides)
14/12/2012: Talk at IRISA / DGA (slides)
25/06/2012 - 29/06/2012: seminar CP meets CAV
28/05/2012 - 01/06/2012: Presentation of our paper on array constraints at CPAIOR 2012 (slides)
29/01/2012 - 03/02/2012: Dagstuhl seminar "Analysis of executables: benefits and challenges" (slides, report)
26/01/2012: Intermediate evaluation of the ANR BINCOA project
11/01/2012: Lecture at the School of Software Verification (ENS Lyon)
15/11/2011: Talk at ENSTA (VMCAI 2011 paper)
18/10/2011: PhD positions and internships are available for 2012, have a look
26/08/2011: Invited speaker at SSV 2011 (slides)
18/07/2011: Presentation of our paper on the BINCOA framework at CAV 2011 (slides, paper)
10/06/2011: Presentation of our work on CFG reconstruction from executable files at GDR GPL (slides)
25/03/2011: Workshop CSTVA 2011, co-located with ICST 2011
24/01/2011: Presentation of our paper on CFG reconstruction from executable files at VMCAI 2011 (slides, paper)

Contrats de recherche

Présent

Projet ANR BinCoA (2009-2012) [analyse de code binaire] [coordinateur principal]

CEA, Paris 7, Bordeaux 1, EdF, Hispano-Suiza, Trusted Labs

Passé

Contrat CEA - EDF (2006-2011) [analyse de code binaire]
Projet Usine Logicielle/ModriVal du pôle SYSTÉM@TIC (2006-2008) [analyse de code binaire]

CEA, INRIA, Paris 6, Orsay, Supélec,
EdF, Hispano-Suiza, Dassault, EADS, Esterel, CS, Trialog

Projet RNTL Avérilès (2005-2008) [systèmes à mémoire dynamique]

ENS Cachan, Paris 7, Grenoble, Cril Technology, EdF

Projet ACI Persée(2002-2006) [systèmes infinis hétérogènes]

ENS Cachan, Paris 7, Bordeaux 1

Contrat ENS Cachan - EDF (2002-2004) [systèmes à mémoire dynamique]

Publications

Logiciels

OSMOSE (depuis 2006) [test automatique de codes binaires]
FAST et FASTeR (2002-2006) [model checking de systèmes à compteurs non bornés]

Sujets de postdocs, thèses et stages

Je suis toujours à la recherche de candidats motivés. N'hésitez pas à me contacter.
Liste de propositions.

Enseignement

Durant ma thèse de doctorat, j'ai été moniteur à l'ENS Cachan. Je donne maintenant des vacations dans divers établissements.

Présent

Test de logiciels -- 44h, cours et tds, niveau M2, Uni. Paris Diderot
Test de logiciels -- 6h, séminaire d'introduction, ENS Lyon
Introduction au model checking -- 15h, cours et tds, niveau M2, École Polytechnique
Introduction au model checking -- 14h, cours et tds, niveau M1, ENSTA

Passé

Introduction à Maple et à l'informatique -- 50h, cours et tds, Classes Préparatoires
Calculabilité -- 20h, tds, ENS Cachan
Logique et programmation logique -- 35h, tds et projet, ENS Cachan
Compilation et typage -- 64h, tds et projet, ENS Cachan
Programmation Java -- 64h, tds et projets, ENS Cachan
Mise à niveau en C -- 15h, tds, ENS Cachan

Divers

infos sur le séminaire du CEA/LSL dont je m'occupe avec Richard Bonichon
conseils aux (futurs) thésards