I am a master’s student in the MPRI (Paris) program.
My research interests are in formal methods, especially:

• Automata & logic — foundations for specifying and reasoning about systems
• Verification — model checking and proof-based methods for correctness
• Complex systems — applying formal guarantees to software, concurrent, and AI-related systems

I am motivated by bridging theoretical models and verification tools, aiming for methods with clear correctness and complexity guarantees.

Publications

• S. Demri and T. Gu. Robustness of Constraint Automata for Description Logics with Concrete Domains.
  To appear in CSL 2026 (LIPIcs). [preprint/link coming soon]

Education

• Université Paris-Saclay / ENS Paris-Saclay — Master Parisien de Recherche en Informatique
  2024 – 2026 (expected)
  Focus: logic, formal methods, automata theory, verification, and algorithms

• Université Paris-Saclay — Bachelor’s in Computer Science and Mathematics
  2021 – 2024
  Double degree program combining computer science and mathematics

Internships

• Research Internship — LMF, ENS Paris-Saclay / Université Paris-Saclay
  Spring–Summer 2025 (MPRI M1)
  Supervisor: Stéphane Demri
  Topic: Automata-based decision procedures for description logics with concrete domains

  • Developed a constraint-automata framework for ALCO(D)/ALCI(D) reasoning
  • Proved robustness of the construction and achieved the optimal complexity bound

• Research Internship — LMF, Université Paris-Saclay
  Summer 2024 (Bachelor’s)
  Supervisor: Burkhart Wolff
  Topic: Integrating Isabelle/HOL with the FDR4 model checker

  • Bridged deductive verification (Isabelle/HOL) with model checking (FDR4) via HOL-CSP
  • Implemented import/export pipeline and new Isabelle/Isar commands for end-to-end CSP analysis
  • Applied the tool to case studies such as CopyBuffer and Dining Philosophers