Aurèle Barrière

CNRS Researcher

I am a researcher at CNRS, working in the CASH team in Lyon, France.
My research is centered on the formal verification of programming language implementations, in particular modern regular expression engines and Just-in-Time compilers.
I lead the Linden Regex project, focusing on the formal study of modern regular expressions.
Feel free to reach out if you're a student looking for internships, master thesis, or PhD opportunities!

Previously, I was a Post-Doc at EPFL, working with Clément Pit-Claudel in the SYSTEMF lab, where I worked on matching algorithms, semantics and proofs for modern regular expressions.
Before that, My PhD was about the formal verification of Just-in-Time (JIT) compilation, with Sandrine Blazy and David Pichardie. I designed a methodology to write and prove the correctness of JIT compilers in Coq, and I developed formally verified prototype JITs in Rocq.

Github. DBLP. Scholar.

aurele.barriere [at] epfl.ch

Publications

• POPL 2026 Formal Verification for JavaScript Regular Expressions:
  a Proven Semantics and its Applications.
  Aurèle Barrière, Victor Deng, Clément Pit-Claudel.
  Distinguished Paper Award.
  Paper. Extended Version. Rocq Development. Artifact. Recorded Talk.
• ACM Book, 2025 Formal Verification of Just-in-Time Compilation.
  Aurèle Barrière.
  Link.
• ICFP 2024 A Coq Mechanization of JavaScript Regular Expression Semantics.
  Noé De Santo, Aurèle Barrière, Clément Pit-Claudel.
  Paper. Coq Development. Artifact. Recorded Talk.
• PLDI 2024 Linear Matching of JavaScript Regular Expressions.
  Aurèle Barrière, Clément Pit-Claudel.
  Paper. OCaml Development. Artifact. Recorded Talk.
• POPL 2023 Formally Verified Native Code Generation in an Effectful JIT:
  Turning the CompCert Backend into a Formally Verified JIT Compiler.
  Aurèle Barrière, Sandrine Blazy, David Pichardie.
  Paper. Coq Development. Artifact. Recorded Talk.
• PhD Thesis, 2022 Formal Verification of Just-in-Time Compilation.
  Aurèle Barrière.
  Thesis supervisors: Sandrine Blazy and David Pichardie.
  My thesis won the EAPLS Best PhD Dissertation Award.
  Thesis Dissertation. Coq Development. Defense Recording.
• POPL 2021 Formally Verified Speculation and Deoptimization in a JIT compiler.
  Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek.
  Paper. Coq Development. Artifact. Recorded Talk.
• CoqPL 2020 (Workshop) Towards Formally Verified Just-in-Time Compilation.
  Aurèle Barrière, Sandrine Blazy, David Pichardie.
  Extended Abstract. Recorded Talk.
• AAMAS 2019 Reasoning about Changes of Observational Power in Logics of Knowledge and Time.
  Aurèle Barrière, Bastien Maubert, Aniello Murano, Sasha Rubin.
• KR 2018 (Extended Abstract) Changing Observations in Epistemic Temporal Logic.
  Aurèle Barrière, Bastien Maubert, Aniello Murano, Sasha Rubin.

Talks

• January 2026. Formal Verification for JavaScript Regular Expressions. POPL'26. Recorded Talk.
• August 2025. Exploring JavaScript Regular Expressions: matching algorithms, mechanized semantics, and formal verification. TC39-TG5 meeting.
• September 2024. A Coq Mechanization of JavaScript Regular Expression Semantics. ICFP'24. Recorded Talk.
• June 2024. Linear Matching of JavaScript Regular Expressions. PLDI'24. Recorded Talk.
• January 2023. Formally Verified Native Code Generation in an Effectful JIT. POPL'23. Recorded Talk.
• December 2022. Formal Verification of Just-in-Time Compilation. Meta, Paris.
• May 2022. Verified Native Code Generation in a Just-in-Time Compiler. Cambium Seminar.
• November 2021. Verified Native Code Generation in a Just-in-Time Compiler. Journée Hybride LVP du GDR GPL.
• January 2021. Formally Verified Speculation and Deoptimization in a JIT compiler. POPL'21. Recorded Talk.
• June 2020. Proving Just-in-Time Compilation Correct. Northeastern NUPRL Seminar.
• January 2020. Towards Formally Verified Just-in-Time Compilation. CoqPL'20. Extended Abstract. Recorded Talk.

Service

• POPL 2026 Student Volunteer Co-Chair.
• Rocqshop 2025 Program Committee.
• ICFP 2025 Program Committee.
• PriSC 2025 Program Committee.
• PLDI 2024 SRC Program Committee and Local Arrangements Co-Chair.
• OOPSLA 2024 Artifact Evaluation Committee.
• OOPSLA 2022 External Review Committee.
• OOPSLA 2022 Artifact Evaluation Committee.

I was a subreviewer for CPP 2026, CPP 2025, ESOP 2024, ESOP 2023 and ITP 2022.

Supervision

I have contributed to the supervision of the following students:

• Victor Deng. PhD student, 2025. Complexity of modern regex matching problems.
• Marcin Wojnarowski. Masters thesis, 2025. Formally verified regex matching optimizations and extensions.
• Théo Hollender. Masters project, 2025. Algorithmic extensions for PikeVM regex matching.
• Zacharie Tevaearai. Masters thesis, 2025. Optimizing regex compilers.
• Victor Deng. Masters internship, 2025. Inductive semantics for JavaScript regexes.
• Marcin Wojnarowski and Robin Hänni. Masters project, 2025. Matching algorithms for Rust regexes.
• Eugène Flesselle. Masters project, 2024. Formally verified regex optimizations.
• Martin Crettol. Bachelors project, 2024. Conformance checking for mechanized specifications.
• Sophie Ammann. Masters thesis, 2024. Formal verification of memoized regex backtracking.
• Zacharie Tevaearai. Masters project, 2024. Regex to WASM compilation.
• Erik Giorgis. Masters project, 2024. RE2 implementation of NFA simulation extensions.
• Alexandre Pinazza. PhD student, 2023. Coq verification of a regex compiler for NFA simulation.
• Noé De Santo. Masters thesis, 2023. Coq mechanized specification of ECMAScript regexes.
• Ludovic Mermod. Master student assistant, 2023. Implementation of regex matching algorithms in the V8 NFA simulation engine.
• Thomas Houhou. Bachelors project, 2023. Development of a semantic-aware JavaScript regex fuzzer.
• Roméo La Spina. Masters project, 2021. Improvements to the inlining pass and adding a liveness analysis for more efficient speculation in a formally verified JIT compiler.

Teaching

• 2024-2025 Interactive Theorem Proving. Lecturer.
• 2019-2022 SEM An introduction to Coq, program semantics and compiler verification. Lecturer.
• 2021-2022 Preparing students for the Agrégation teaching degree. Preparing and supervising programming labs.
• 2019-2021 GEN Software engineering. Teaching Assistant.
• 2020-2021 ACF Software Formal Analysis and Design. Teaching Assistant.

Research Internships

• 2019 IRISA, Rennes. Formally Verified Just-in-Time Compilation.
  Supervisors: Sandrine Blazy and David Pichardie. Internship Report.
• 2018 Princeton University. VST Verification of a B+Trees Library.
  Supervisor: Andrew Appel. Internship Report.
• 2017 University Federico II, Napoli. Changing Observation in Epistemic Temporal Logics.
  Supervisors: Aniello Murano, Bastien Maubert and Sasha Rubin. Internship Report.
• 2017 Software Foundations Laboratory, Seoul National University. Implementing Integer-Pointer Cast Semantics in CompCert.
  Supervisor: Chung-Kil Hur. Internship Report.
• 2016 IRISA, Rennes. Worst Case Execution Time (WCET) estimation using Abstract Interpretation and Constraint Programming.
  Supervisors: Charlotte Truchet and David Cachera. Internship report (in French).