Supervision

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

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

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

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