Sébastien BARDIN Researcher in Computer Science
	Education Ph.D. in Computer Science, ENS Cachan (France), 2005 M.S. in Computer Science, ENSIIE (France), 2002 Current position Researcher, Software Safety and Security Lab., Commissariat à l'Energie Atomique (CEA),  Paris-Région, France Contact information Email    : sebastien.bardin(at)cea.fr Phone   : +33 (0)1 69 08 54 16 Address: CEA NanoInnov                  91191 Gif sur Yvettes, France

Research Interests

• Main areas: validation and verification, software engineering, formal methods, program verification, model verification
• Subfields:  (software) model checking, automatic testing, concolic execution
• Application domains:  embedded systems, critical systems, computer security, software productivity
  

Verification of machine code 

• Automatic recovery of a behavioural model of an executable file and  automatic test data generation
• Concolic execution
• Prototype OSMOSE (slides)
  
• Prototype CFGBuilder [safe CFG recovery]  (slides)    
  
• DBA formal model and DBA Toolkit   (slides)
• BINSEC

Model checking systems with infinite state-space (past)

• Counter systems,  pointer systems, heterogeneous systems
• Symbolic representations for infinite sets and acceleration to unfold loops
• Software FAST and FASTeR  [model checking of (unbounded) counter systems]  
  

News

• [upcoming]  05/09/2016 - 09/09/2016: The 22th International Conference on Principles and Practice of Constraint Programming CP 2016   -- including a Testing and Verification track
  
• [upcoming]  05/09/2016: The 3rd CP meets Verification workshop, co-located with CP 2016   -- [deadline for abstract: 27/06/2016]
• [upcoming]  01/08/2016 - 03/08/2016:  IEEE International Conference on Software Quality, Reliability & Security QRS 2016 
  
• [upcoming]  18/07/2016 - 20/07/2016:  ISSTA 2016  (paper on concretisation/symbolization policies in Dynamic symbolic Execution)
  
• [upcoming]  07/07/2016: Summer School on Cybersecurity (invited talk)
  
• [upcoming]  04/07/2016 - 06/07/2016: RMLL Security Track  (slides)
  
• [upcoming]  08/06/2016 : AFADL 2016 (Besançon) (slides)
• 14/03/2016 - 18/03/2016:  Presentation of our  new Dynamic Symbolic Execution engine at SANER 2016 
• 02/03/2016: Workshop Digital Trust  Université d'Auvergne (invited talk)
  
• 05/11/2015: Presentation of our work on labels and symbolic execution at CFV 2015 (slides)
• 08/09/2015: Workshop on Security for Low-Level Code, colocated with SAS 2015

• 01/08/2015: Workshop LOCAS 2015 (binary-level security analysis), colocated with CADE-25
  
• 01/07/2015: Talk at Imperial College about combining static and dynamic analyses (slides)
• 23/06/2015: Workshop USE 2015 (symbolic execution), colocated with FM 2015.  (slides of our invited talk)
  
• 09/06/2015-10/06/2015: Presentation of sound detection of infeasible test requirements at AFADL 2015
• 19/05/2015-22/05/2015:  Presentation of the BINSEC project at RESSI 2015
  
• 11/04/2015-18/04/2015: Presentation of a tool paper on binary-level analysis at TACAS 2015
  
• 13/04/2015-17/04/2015: Presentation of sound detection of infeasible test requirements at ICST 2015  (slides)
• 13/03/2015:  Frama-C Day at CEA LIST
  
• 02/03/2015-05/03/2015: NII Shonan meeting (Low-level code analysis)
• 07/01/2015-10/01/2015: Presentation of preliminary work on static analysis of temporal properties in Frama-C at JFLA 2015
  
• 27/10/2014 - 30/10/2014: Dagstuhl seminar "Symbolic Execution and Constraint Solving" (slides)
  
• 08/09/2014: Workshop CP meets CAV

Projects

Current

• Projet ANR BINSEC (2013-2017) [binary-level security analysis] [project leader]    
• CEA, IRISA, LORIA, VERIMAG, EADS IW, VUPEN
• Projet ANR SOPRANO (2015-2018) [combination of solvers for verification]
• CEA, INRIA, Uni. Paris-Sud, AdaCore, OCaml Pro
• Projet DGA SASSE (2013-2016)
  
• AMOSSYS, CEA

Past

• Project ANR BinCoA (2009-2012) [machine code analysis] [project leader]
• funded by the French Research Agency 
• CEA, Uni. Paris 7, Uni. Bordeaux 1, EdF, Hispano-Suiza, Trusted Labs 
  
• Contract CEA - EDF  (2006-2011) [machine code analysis]
• Project  Usine Logicielle/ModriVal (2006-2008) [machine code analysis]
• funded by the French Research Agency 
• CEA, INRIA, Uni. Paris 6, Uni. Orsay, Supélec, 
• EdF, Hispano-Suiza, Dassault, EADS, Esterel, CS, Trialog   
• Project RNTL Avérilès (2005-2008) [verification of systems with dynamic memory allocation]
• funded by the French Research Agency 
• ENS Cachan, Uni. Paris 7, Verimag, Cril Technology, EdF
• Project ACI Persée (2002-2006) [verification of heterogeneous infinite-state systems]
• funded by the French Research Agency 
• ENS Cachan, Uni. Paris 7, Uni. Bordeaux 1
• Contract ENS Cachan - EDF [verification of systems with dynamic memory allocation]

Publications

• Publication list
• DBLP
• Google Scholar

Software

• BINSEC                    (since 2012)  [binary-level program analysis]
  
• OSMOSE                  (2006-2011)  [automatic executable testing]
• FAST and FASTeR  (2002-2006)  [counter system model checking]

Postdocs, PhDs and trainee proposals

Teaching

Current

• Software model checking -- 10h, Uni. Paris Saclay
• Software testing and symbolic execution -- 10h, Uni. Strasbourg
• Formal methods and software testing -- 20h, INSA Val de Loire
  

• Basis of model checking (École Polytechnique, ENSTA)
• Software testing (Uni. Paris Diderot)
• Quick introduction to numerical analysis, algorithmic and Maple (Classes Préparatoires)