• Teaching
• Head of the Cyber-security track (parcours cyber-sécurité in french) of the second year of Master in Computer Science (M2) Since 2023.
• Co-Head of the Research track of the first year of Master in Computer Science (M1) 2013-2021.
• Head of first year of Master in Computer Science (M1) 2009-2012.


• L1: Algorithmic and complexity analysis (theoretical and practical point of view). See the ACE page (in french and restricted access)
• L3: Security of software and protocols (Cryptographic protocol verification in Proverif and implementation in Typescript). See SECU (in french and restricted access).
• M1: 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).
• M2: A short course on the Ethereum blockchain and Solidity programming. See the BLK page.


• Software Engineering (2014-2023). You can find here teaching material including videos, slides, etc. (in french)
• Functional programming
• Object Oriented Programming, UML, Design patterns
• 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: 2023/07/11