Supervision

PhD

• Florent Krasnopol — 2025–2028
  Automated Theorem Proving over the Reals for Reasoning on Quantum Circuits
  With Stephan Merz and Sophie Tourret

Master’s Thesis

• Ayath Abogounrin, Guillaume Potel, and Matheo Vigneres — 2026
  Indexing Structures for First-Order Logic | 1st year of master
  With Marie Duflot-Kremer and Engel Lefaucheux

• Claude Leroy — 2025-2026
  Decentralized Diagnosis of Stochastic Systems | 1st year of master
  With Engel Lefaucheux

Bachelor’s Thesis

• Johann Rosain — 2021-2022
  Deduction Modulo Theory and Polymorphism in Goéland
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

• Cédric Berthet, Enzo Goulesque, Lorenzo Puccio, Margaux Renoir, and Tom Simula — 2021-2022
  Integration of Arithmetic Reasoning in Goéland
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

Internship

• Ruka Hlupic — 2026
  Automated Reasoning for Nikoli’s games | 2nd year of bachelor
  With Florent Krasnopol

• Corentin Minaroli — 2026
  Unification in Goeland | 3rd year of bachelor

• Nicolas Schutz-Kuchly — 2026
  Equality Reasoning in Goeland | 3rd year of bachelor

• Titouan Le Pen — 2025
  Development of a Resolution-Based Automated Theorem Prover | 2nd year of bachelor

• Achille Razafimaharo — 2025
  Development of a Tableau-Based Automated Theorem Prover | 2nd year of bachelor

• Filip Jagiellowicz — 2024
  Implementation of a Decision Procedure for CaAL | 1st year of master
  With Philipp Rümmer

• Dylan Bettendroffer — 2023
  A Dedukti Output for Goéland | 2nd year of master
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

• Johann Rosain — 2023
  Deskolemization in First-Order Logic | 3rd year of bachelor
  With David Delahaye, Olivier Hermant and Simon Robillard

• Matthieu Pierret — 2023
  Interactive Proof in Goéland | 2rd year of bachelor
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

• Lorenzo Puccio — 2022
  A Rocq Output for Goéland | 3rd year of bachelor
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

• Adrien Mecibah — 2022
  Interactive Traces for ATP | 2nd year of bachelor
  With David Delahaye, Hinde Lilia Bouziane and Simon Robillard

• Nina Janeva — 2021
  Design of an Automated Tool for Benchmarks | 3rd year of bachelor
  With David Delahaye and Hinde Lilia Bouziane

• Johann Rosain — 2021
  Code Trees for Unification | 2nd year of bachelor
  With David Delahaye and Hinde Lilia Bouziane