• Teaching
• Head of first year of Master in Computer Science (M1) 2009-2012.
• Co-Head of the Research track of the first year of Master in Computer Science (M1) 2013-2021.
• Algorithmic and complexity analysis. See the SI1/Spé Info 1 page (in french and restricted access)
• Software Engineering. See the GEN page (in french)
• Functional programming
• Object Oriented Programming, UML, Design patterns
• Formal Methods (B and Why frameworks, PVS and Isabelle/HOL proof assistants). See the ACF page (Lecture on Formal Design using Isabelle/HOL and Scala).
• A short course on the Ethereum blockchain and Solidity programming. See the BLK page.
• First order logic, rewriting and proof by induction in proof assistants
• Introduction to cryptographic Protocols and their verification. (If you are french speaking, you can find here Teaching material)

• Research Themes
• Verification
• Term Rewriting
• Tree Automata
• Reachability analysis over Term Rewriting Systems (Have a look to my Habilitation document on this subject)
• Cryptographic Protocol Verification (see a video tutorial on the subject)
• Blockchains and smart contract semantics
• Tools and projects
• Ethereum Formal Semantics for Gas Consumption Analysis
• : a tree automata library  (in OCaml)  for achieving reachability analysis over Term Rewriting Systems
• : a Security Protocol ANimator for AVISPA (see a video tutorial)
• Copster: COmpiling Program Semantics into TErm Rewriting
  
• Projet ANR RAVAJ : Rewriting and Approximations for Verification of Java Applets

• Publications

Last Modified: 2022/03/07