About

I'm a Post-Doc at EPFL, in the SYSTEMF lab.

Résumé. Github. DBLP.

Contact

aurele.barriere [at] epfl.ch

Publications

  • PLDI'24 Aurèle Barrière, Clément Pit-Claudel.
    Linear Matching of JavaScript Regular Expressions.
    Pre-print. OCaml Development.
  • PhD Thesis Aurèle Barrière.
    Formal Verification of Just-in-Time Compilation.
    Thesis supervisors: Sandrine Blazy and David Pichardie.
    Thesis Dissertation. Coq Development. Defense Recording.
  • POPL'23 Aurèle Barrière, Sandrine Blazy, David Pichardie.
    Formally Verified Native Code Generation in an Effectful JIT:
    Turning the CompCert Backend into a Formally Verified JIT Compiler.
    Pre-print. Coq Development. Recorded Talk.
  • POPL'21 Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek.
    Formally Verified Speculation and Deoptimization in a JIT compiler.
    Pre-print. Coq Development. Recorded Talk.
  • CoqPL'20 Aurèle Barrière, Sandrine Blazy, David Pichardie.
    Towards Formally Verified Just-in-Time Compilation.
    Slides. Extended Abstract.
  • AAMAS'19 Aurèle Barrière, Bastien Maubert, Aniello Murano, Sasha Rubin.
    Reasoning about Changes of Observational Power in Logics of Knowledge and Time.
  • KR'18 Aurèle Barrière, Bastien Maubert, Aniello Murano, Sasha Rubin.
    Changing Observations in Epistemic Temporal Logic. - Extended Abstract.

Drafts:

  • 2024 Noé De Santo, Aurèle Barrière, Clément Pit-Claudel.
    A Coq Mechanization of JavaScript Regular Expression Semantics.
    First version.

Talks

  • May 2022. Aurèle Barrière, Sandrine Blazy, David Pichardie. Verified Native Code Generation in a Just-in-Time Compiler. Cambium Seminar. Slides.
  • November 2021. Aurèle Barrière, Sandrine Blazy, David Pichardie. Verified Native Code Generation in a Just-in-Time Compiler. Journée Hybride LVP du GDR GPL. Slides.
  • June 2020. Aurèle Barrière, Sandrine Blazy, David Pichardie. Proving Just-in-Time Compilation Correct. Northeastern NUPRL Seminar.
  • January 2020. Aurèle Barrière, Sandrine Blazy, David Pichardie. Towards Formally Verified Just-in-Time Compilation. CoqPL 2020. Slides. Extended Abstract.

Program Committees

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

Supervision

I have contributed to the supervision of the following students:

  • 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

2021-2022

  • Preparing students for the Agrégation teaching degree.
  • SEM An introduction to Coq, program semantics and compiler verification.

2020-2021

  • GEN Software engineering.
  • ACF Software Formal Analysis and Design.
  • SEM

2019-2020

Research Internships

2019 Internship

In 2019, I did an internship at IRISA, about formal verification of just-in-time compilation. This work was supervised by Sandrine Blazy and David Pichardie. Internship Report.

2018 Internship

In 2018, I did an internship at Princeton University, about verifying a B+Trees Library using VST. This work was supervised by Andrew Appel and part of the DeepSpecDB project. Internship Report.

2017 Winter Internship

In Winter 2017, I did an internship in the University Federico II in Naples, about Changing Observation in Epistemic Temporal Logics. This internship was supervised by Aniello Murano, Bastien Maubert and Sasha Rubin. Internship Report.

2017 Summer Internship

In Summer 2017, I did an internship with the Software Foundations Laboratory in Seoul National University, about implementing integer-pointer cast semantics in CompCert. This internship was supervised by Chung-Kil Hur. Internship Report.

2016 Internship

In 2016, I did an internship in the CELTIQUE team (IRISA Rennes), on high level Worst Case Execution Time (WCET) estimation using Abstract Interpretation and Constraint Programming. This internship was supervised by Charlotte Truchet and David Cachera. Internship report (in French).