Postdocs, PhDs, Master thesis and trainee proposals

Preliminaries

• My institution (CEA) offers a pool of internship / Phd / Postdoc positions each year, so getting a grant is possible for excellent candidates. 
• We are primarily looking for highly motivated, passionated and hard-working people, with a clear background in Computer Science
  
• comfortable with both theoretical and practical aspects of CS -- maths and programming
  
• knowledge in at least one of the following topics: formal methods, security, compilers, logic and theorem proving, artificial intelligence and machine learning
  
• knowledge in functional programming and OCaml is a plus 
• If you are interested in my current research themes but not in my current proposals, don't hesitate to contact me: we may agree on a research direction that suites both of us
  

Postdocs

• binary-level verification techniques, with application to security analysis (vulnerabilities, malware, reverse, code hardening, ...)
  
• dedicated constraint resolution  and SMT solving methods for program analysis and software verification
  
• security-oriented program analysis and machine learning
  

PhD topics

Master thesis-Trainees  (level: L3, M1, M2)

Current and former students/postdocs

Postdoc

• Christophe Chareton [2018-2019] Formal methods for quantum programs
  
• Michael Marcozzi [2015-2017]  Hyperproperty testing
  
• Mickaël Delahaye [2014-2015] A unified framework for automatic white-box testing
  

PhD students

• Soline Ducoussot [2020-...] Attackers in code analysis
• Guillaume Girol [2019-...] Constraint solving for security
  
• Grégoire Menguy [2019-...] Code contract inference
  
• Lesly-Ann Daniel [2018-...] Software analysis of non-interference properties
  
• Mathilde Ollivier [2017-...] Software protection against semantic attacks
  
• Yaëlle Vinçont [2017-...] Smart fuzing
  
• Manh Dung Nguyen [2017-...] Advanced vulnerability analysis
• Frédéric Recoules [2017-...] Formal analysis of inline assembly code

• Benjamin Farinier [2015-2020] Constraint solving for security
• Jonathan Salwan [2015-2020] Binary-level code analysis for security
• Adel Djoudi [2013-2016]  Safe static analysis  of executables
  
• Robin David [2013-2016] Automatic analysis of obfuscated executables
  

Master students

• Oliver Stuart Constant [2020, Ecole Polytechnique, 6 months] CFI protections
  
• Cauim de Souza Lima [2019, Ecole Polytechnique, 6 months] Machine Learning for bypassing code protections
  
• Lesly-Ann Daniel [2018, ENS Rennes, 6 months]  Symbolic execution for hyper-properties
  
• Yaëlle Vinçont [2017, Uni. Paris-Sud, 6 months] Smart fuzzing
  
• Guillaume Girol [2017, Ecole Polytechnique, 4 months]  Efficient symbolic execution
  
• Hai Nguyen Van [2014, Uni. Paris 7, 6 months] Syntactic verification through model checking
  
• Guillaume Jeanne [2014, ENSIMAG, 6 months] Automatic crash analysis
• Hai Van Nguyen [2014, Uni. Paris 7, 6 months] Syntactic model checking
  
• Simon Collet [2013, Centrale Lyon, 6 months] Efficient constraint resolution for subclasses of SAT
  
• Quentin Plazar [2013, Supélec Metz, 6 months] Static analysis of self-modifying code
  
• Hai Van Nguyen [2013, Uni. Paris 7, 3 months] Malware detection
  
• Théo Dzierzbicki [2012, INSA Lyon, 4 months] Verification-oriented decompilation
  
• Olivier Fahy [2012, Uni. Versailles Saint-Quentin, 6 months] A study of IDA Pro: possibilities, limits, extensions through static analysis plugin
  
• François Cheynier  [2011, ENSIIE, 3 months] Mutation testing as predicate coverage
  
• Nicolas Cornuet [2011, Uni. Orsay, 6 monts, co-supervisor] Binary-based coverage  vs source-based coverage: an empiric evaluation of common criteria
  
• Pei-Yu  [2010, IRISA, 6 months]  Combining Constraint Programming and SMT for solving formulas over large arrays 
• Baya Ait Abdelmalek [2008, Uni. Paris 7, 6 months]  Modelling x86 into OSMOSE
• Florian Perroud [2008, Uni. Marseilles, 6 months]  Design and implementation of a GUI for OSMOSE