MPRI defense schedule 2026

All defenses will take place in room 1002, Sophie Germain building.

Defenses are public. Discussions during breaks are restricted to the advisors and members of the jury.

Information about how to prepare your report and your defense can be found here.

Morning session. Jury: Christoph Dürr, Brice Minaud, Sylvain Schmitz.

• 09:30>10:00 - Florent Ferrari: “Soundness of Rust Verification in the Presence of Safe and Unsafe Code”, with Yannick Zakowski. Reviewer: Sylvain Schmitz.
• 10:00>10:30 - Noémie Fong: “étude empirique, théorique et prospective du langage des expressions Nix”, with (Tito) Nguyễn Lê Thành Dũng. Reviewer: Sylvain Schmitz.
• Break.
• 11:00>11:30 - Basile Schlosser: “Memory Models for the Computationally Complete Symbolic Attacker”, with Guillaume Scerri. Reviewer: Brice Minaud.
• 11:30>12:00 - Maëlle Cornely: “Certified Compilation of Concurrent C Programs”, with Jean-Marie Madiot. Reviewer: Sylvain Schmitz.
• 12:00>12:30 - Hubert Gruniaux: “Vérification d'allocateurs mémoire par analyse statique”, with Xavier Rival. Reviewer: Sylvain Schmitz.

Afternoon session. Jury: Christoph Dürr, Brice Minaud, Sylvain Schmitz.

• 14:00>14:30 - Paul Adam: “Rendu d’applications web pour smartphone low-tech”, with Martin Quinson. Reviewer: Christoph Dürr.
• 14:30>15:00 - Noémie Catherinot: “Online Bipartite Matching with Offline Agents and Online Items”, with Simon Mauras. Reviewer: Christoph Dürr.
• 15:00>15:30 - Sélène Corbineau: “Fast Evaluation of Elementary Functions with Medium Precision”, with Marc Mezzarobba. Reviewer: Christoph Dürr.
• Break.
• 16:00>16:30 - Gabriel Desfrene: “Relational Separation Logic for Compiler Verification”, with François Pottier. Reviewer: Sylvain Schmitz.
• 16:30>17:00 - Doan-Dai Nguyen: “Asymptotic Optimality in Stochastic Non-Bipartite Matching”, with Ana Bušić. Reviewer: Christoph Dürr.
• 17:00>17:30 - Salwa Tabet Gonzalez: “Formal Proof of a LTI Systems Invariants Computation Approach”, with Maxime Jacquemin. Reviewer: Sylvain Schmitz.

Morning session. Jury: Brice Minaud, François Pottier, Sylvain Schmitz.

• 09:30>10:00 - Viraj Agashe: “Evaluation of Sequence-Based Conflict-Free Replicated Data Types (CRDTs)”, with Claudia-Lavinia Ignat. Reviewer: François Pottier.
• 10:00>10:30 - Mathilde Kermorgant: “Lattice Short Secret Sharing”, with Thomas Espitau. Reviewer: Brice Minaud.
• Break.
• 11:00>11:30 - Wassel Bousmaha: “Applications of Trocq to Computational Refinements of Mathematical Algorithms”, with Cyril Cohen. Reviewer: François Pottier.
• 11:30>12:00 - Gaëtan Regaud: “Reactive synthesis for systems with data from modal mu-calculus specifications”, with Léo Exibard. Reviewer: Sylvain Schmitz.
• 12:00>12:30 - Tom Soucies: “Formally Verified Compilation of an Interaction-Oriented Programming Language”, with Basile Pesin. Reviewer: Sylvain Schmitz.

Afternoon session. Jury: Brice Minaud, François Pottier, Sylvain Schmitz.

• 14:00>14:30 - Hugo Barreiro: “Jasmin on Wasm”, with Manuel Serrano. Reviewer: François Pottier.
• 14:30>15:00 - Youcef Bouzid: “Symbolic Execution at Scale via Efficient Memory Summaries”, with Sébastien Bardin. Reviewer: François Pottier.
• 15:00>15:30 - Antonin Bretagne: “Gradual and Semantic Typing for Elixir's Module System”, with Giuseppe Castagna. Reviewer: François Pottier.
• Break.
• 16:00>16:30 - Jean-Baptiste Menant: “Compilation formellement vérifiée à l'aide d'E-Graphs”, with David Monniaux. Reviewer: François Pottier.
• 16:30>17:00 - Florian Chivé: “Interactive Program Verification Meets Abstract Interpretation”, with Aymeric Fromherz. Reviewer: François Pottier.
• 17:00>17:30 - Viviane Ledoux: “Apprentissage d'un mouvement de redressement avec un robot bipède à roues”, with Nicolas Perrin-Gilbert. Reviewer: Brice Minaud.

Morning session. Jury: Jean Goubault-Larrecq, Sophie Laplante, Brice Minaud.

• 09:30>10:00 - Loïc Chevalier: “Verified Translation of Pointer Arithmetic from C to safe Rust”, with Aymeric Fromherz. Reviewer: Jean Goubault-Larrecq.
• 10:00>10:30 - Arthur Adjedj: “The Expression Problem for Mechanised Proofs”, with Yannick Forster. Reviewer: Jean Goubault-Larrecq.
• Break.
• 11:00>11:30 - Zhenghao Hu: “Solvability of majority consensus task”, with Jérémy Ledent. Reviewer: Brice Minaud.
• 11:30>12:00 - Vincent Jules: “Tree Edit Distance”, with Panagiotis Charalampopoulos. Reviewer: Sophie Laplante.
• 12:00>12:30 - Claire Sintzoff: “Chiffrement dans les groupes de classes et preuves zero-knowledge”, with Fabien Laguillaumie. Reviewer: Sophie Laplante.

Afternoon session. Jury: Jean Goubault-Larrecq, Brice Minaud, Gilles Schaeffer.

• 14:00>14:30 - Vincenzo Politelli: “Bijections pour le cartes nonorientables”, with Jérémie Bettinelli. Reviewer: Gilles Schaeffer.
• 14:30>15:00 - Valentin Defransure: “Quantum Speedups for Planted Inference Problems: Algorithmic and Cryptographic Implications for Post-Quantum Security”, with Yixin Shen. Reviewer: Brice Minaud.
• 15:00>15:30 - Maël Hostettler: “Algebraic Cryptanalysis of PRNGs”, with Gregor Leander. Reviewer: Brice Minaud.
• Break.
• 16:00>16:30 - Louis Lachaize: “Propriétés combinatoires et calculatoires des hom shifts”, with Benjamin Hellouin de Menibus. Reviewer: Gilles Schaeffer.
• 16:30>17:00 - Zacharoula Sotiriou: “Mobile Agent Algorithms in Limited Communication Models”, with Evangelos Bampas. Reviewer: Gilles Schaeffer.
• 17:00>17:30 - Arthur Bertrand: “Schnyder Woods for Higher Genus Surfaces”, with Luca Castelli Aleardi. Reviewer: Gilles Schaeffer.

Morning session. Jury: Jean Goubault-Larrecq, Brice Minaud, François Pottier.

• 09:30>10:00 - Coda Bourotte: “Reduction Graphs in the Linear λ-Calculus”, with Giulio Manzonetto. Reviewer: Jean Goubault-Larrecq.
• 10:00>10:30 - Yago Iglesias Vazquez: “Design and Verification of Multiword Floating-Point Arithmetic”, with Sylvie Boldo. Reviewer: Jean Goubault-Larrecq.
• Break.
• 11:00>11:30 - Erin Le Boulc'h: “Contenu logique des critères de correction des réseaux de preuve de la logique linéaire : Séquentialisation, interpolation et recherche de preuve”, with Alexis Saurin. Reviewer: Jean Goubault-Larrecq.
• 11:30>12:00 - Felix Sassus-Bourda: “Primitive Types and Verified Erasure in Rocq and MetaRocq”, with Matthieu Sozeau. Reviewer: François Pottier.
• 12:00>12:30 - Giuseppe Spriano: “Decoding of Sum-Rank Metric Codes”, with Ferdinando Zullo. Reviewer: Brice Minaud.

Afternoon session. Jury: Jean Goubault-Larrecq, Brice Minaud, François Pottier.

• 14:00>14:30 - Yoshimi-Theophile Etienne: “Local Extensions of Type Theory”, with Théo Winterhalter Théo. Reviewer: Jean Goubault-Larrecq.
• 14:30>15:00 - Léo Lanteri Thauvin: “Böhm Trees for the Bang Calculus”, with Delia Kesner. Reviewer: Jean Goubault-Larrecq.
• 15:00>15:30 - Fernando Leal Sanchez: “Formalizing Higher-Order Separation Logic in Lean”, with Ralf Jung. Reviewer: François Pottier.
• Break.
• 16:00>16:30 - Travis Leblanc: “Exploring the Space-Time Tradeoff in Reversible Abstract Machines for the Untyped Lambda-Calculus”, with Ugo Dal Lago. Reviewer: Jean Goubault-Larrecq.
• 16:30>17:00 - Augustin Rochereau: “Inference of Broadcast Protocols”, with Peter Habermehl. Reviewer: Jean Goubault-Larrecq.
• 17:00>17:30 - Elsa Lubek: “A la recherche du flux logique et linguistique : Catégories de dialogue, TQFT et grammaires catégorielles”, with Paul-André Melliès. Reviewer: Jean Goubault-Larrecq.

Morning session. Jury: Sophie Laplante, Brice Minaud, Hieu Phan.

• 09:30>10:00 - Marwan Azizi: “Cryptographic Simulator Synthesis Using Program Logics”, with Adrien Koutsos. Reviewer: Hieu Phan.
• 10:00>10:30 - Killian Provin: “Post-Quantum Anonymous Credentials”, with Matthieu Rivain. Reviewer: Sophie Laplante.
• Break.
• 11:00>11:30 - Rémi Germe: “Idiomatic Specification of Magic Wands in Implicit Dynamic Frames”, with Müller Peter. Reviewer: Sophie Laplante.
• 11:30>12:00 - Gabrielle Lalou: “Chiffrement avancé fondé sur les problèmes LWE”, with Thomas Ricosset. Reviewer: Hieu Phan.
• 12:00>12:30 - Jules Fraizier: “Design and Analysis of Randomized Heuristic Algorithms”, with Benjamin Doerr. Reviewer: Sophie Laplante.

Afternoon session. Jury: Sophie Laplante, Brice Minaud, Théo Winterhalter.

• 14:00>14:30 - Simon Corbard: “Méta-théorie d’une théorie des types dépendants avec adapteurs”, with Thibault Benjamin. Reviewer: Théo Winterhalter.
• 14:30>15:00 - Mohammadhossein Zaredehabadi: “A Distributed Separator for Minor-Free Graphs”, with Louis Esperet. Reviewer: Sophie Laplante.
• 15:00>15:30 - Julien Marquet: “Mechanizing Synthetic Guarded Domain Theory”, with Paul-André Melliès. Reviewer: Théo Winterhalter.
• Break.
• 16:00>16:30 - Lyes Saadi: “A Syntax for Proof-Relevant Observational Type Theory”, with Loïc Pujet. Reviewer: Théo Winterhalter.
• 16:30>17:00 - Sébastien Very: “Temporal Coloring”, with Mikaël Rabie. Reviewer: Sophie Laplante.
• 17:00>17:30 - Leo Leesco: “Verified Lightweight Static Analyses for Strata”, with Olivier Bouissou. Reviewer: Théo Winterhalter.

Morning session. Jury: Christoph Dürr, Brice Minaud, Hieu Phan.

• 09:30>10:00 - Vladislav de Haldat du Lys: “Vérification des procédures de conduite pour les centrales nucléaires”, with Valentin Rychkov. Reviewer: Christoph Dürr.
• 10:00>10:30 - Dominique Bazin: “Complexité et cryptographie quantique”, with Céline Chevalier. Reviewer: Hieu Phan.
• Break.
• 11:00>11:30 - Quy Dang Ngo: “Sparsification of Matroids with Applications”, with Chien-Chung Huang. Reviewer: Christoph Dürr.
• 11:30>12:00 - Maxence Jauberty: “Study of Optimal Solutions of Delsarte's Linear Program”, with Thomas Debris. Reviewer: Hieu Phan.
• 12:00>12:30 - Alexis Hamon: “Préservation de contre-mesures aux attaques par fautes”, with Vincent Laporte. Reviewer: Hieu Phan.

Afternoon session. Jury: Christoph Dürr, Brice Minaud, Hieu Phan.

• 14:00>14:30 - Milo Horch: “Étude de la marche aléatoire ReCom pour le découpage électoral, analyse de temps de mélange et de la distribution stationnaire dans des cas simplifiés”, with David Saulpic. Reviewer: Christoph Dürr.
• 14:30>15:00 - Guillaume Chirache: “Side-Channel Analysis of a Post-Quantum Encryption Scheme without Re-encryption”, with Mélissa Rossi. Reviewer: Hieu Phan.
• 15:00>15:30 - Edwin Feneux: “Higher-Order MDS Codes”, with Alessandro Neri. Reviewer: Hieu Phan.
• Break.
• 16:00>16:30 - Jules Timmerman: “Composition in the Squirrel Prover”, with Charlie Jacomme. Reviewer: Hieu Phan.
• 16:30>17:00 - Gaby Le Bideau: “Program Synthesis for Loop Bound Inference”, with Gregoire Menguy. Reviewer: Christoph Dürr.
• 17:00>17:30 - Mahdi Nasser: “Efficient Sparse Attention for LLMs Long-Context Inference”, with Zhen Zhang. Reviewer: Hieu Phan.
• 17:30>18:00 - Teiki Rigaud: “Approximation Schemes for Euclidean Capacitated Vehicle Routing”, with Hang Zhou. Reviewer: Christoph Dürr.

Morning session. Jury: Brice Minaud, Gilles Schaeffer, Théo Winterhalter.

• 09:30>10:00 - Gaspard Meunier: “Anamorphic Encryption”, with Hieu Phan. Reviewer: Brice Minaud.
• 10:00>10:30 - Léopold Bernard: “Cryptanalysis of Post-Quantum Signature Schemes (Lattice-Based Cryptography)”, with Saho Uchida. Reviewer: Brice Minaud.
• Break.
• 11:00>11:30 - Andreas Mulard: “Study of Single Transferable Vote Algorithm for Participatory Budgeting”, with Dominik Peters. Reviewer: Gilles Schaeffer.
• 11:30>12:00 - Eliot Collombet: “Protocoles cryptographiques distribués à base d'isogénies”, with Luca De Feo. Reviewer: Brice Minaud.
• 12:00>12:30 - Rémy Kimbrough: “Cutting Surface-Embedded Graphs: Approximation and Parameterization”, with Arnaud De Mesmay. Reviewer: Gilles Schaeffer.

Afternoon session. Jury: Brice Minaud, Gilles Schaeffer, Théo Winterhalter.

• 14:00>14:30 - Abdelkader Belloundja: “Formally Verified Left Recursive Operator Precedence Parser”, with Pierre Courtieu. Reviewer: Théo Winterhalter.
• 14:30>15:00 - Ewen Dufour: “Canonical for Rocq”, with Pierre Boutry. Reviewer: Théo Winterhalter.
• 15:00>15:30 - Amelia Coutard: “Cohérence et évolution des hiérarchies de structures mathématiques en Théorie des Types”, with Sarah Reboullet. Reviewer: Théo Winterhalter.
• Break.
• 16:00>16:30 - Arthur Molina-Mounier: “Singular Euler-Maclaurin Expansion in Rocq”, with Dominik Kirst. Reviewer: Théo Winterhalter.
• 16:30>17:00 - Hadi Fouani: “Mathematical Investigation of Random Switches in Cell Regulation”, with Stefan HAAR. Reviewer: Gilles Schaeffer.
• 17:00>17:30 - Madhav Cherupilil Sajeev: “Integration of Topological and Geometric Approaches in the Context of 3D Modeling”, with Alexandra Bac. Reviewer: Gilles Schaeffer.