EPFL (Lausanne, Switzerland)
2018-2024
Abstract
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the last published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an industrial-strength regex language has been faithfully mechanized in an interactive theorem prover. We highlight interesting challenges that arose in the process (including issues of encoding, corner cases, and executability), and we document the steps that we took to ensure that the result is straightforwardly auditable and that our understanding of the spec aligns with existing implementations.
We demonstrate the usability and versatility of the mechanization through a broad collection of analyses, case studies, and experiments: we prove that JavaScript regex matching always terminates and is safe (no assertion failures); we identify subtle corner cases that led to mistakes in previous publications; we verify an optimization extracted from a state-of-the-art regex engine; we show that some classic properties described in automata textbooks and used in derivatives-based matchers do not hold in JavaScript regex; and we demonstrate that the cost of updating the mechanization to account for changes in the original specification is reasonably low.
Our mechanization can be extracted to OCaml and linked with Unicode libraries to produce an executable engine that passes the relevant parts of the official Test262 conformance test suite.
Others
"Master's Valorization"
March-July 2024
System F (EPFL), Switzerland.
Supervised by Dr. Aurèle Barrière & Prof. Clément Pit-Claudel.
Continued work on Warblre, a mechanization in Coq of JS regex semantics.
Student Intern
March-August 2023
Oracle Labs, Switzerland.
Supervised by Dr. Peter Hofer.
Implemented an almost complete support for the new upcoming foreign functions interface of the Java ecosystem in native-image, an ahead-of-time compiler for Java, and SubstrateVM, its companion runtime.
The implementation fully supports dynamic library loading, calls from Java to native functions, and calls from native to Java methods.
Research Intern
July-September 2022
Supervised by Prof. Viktor Kunčak.
Developed a calculus allowing the elimination of pieces of code (called "ghost") without altering the result or visible effects of a computation.
The calculus notably supports both mutable references and subtyping.
Also investigated the relation between ghost code and the non-interference property, which comes from the domain of security type systems.
Student Assistant
2020-2023
EPFL, Switzerland
For the following classes:
Responsibilities included: presenting labs to students, correcting labs and exams, creating and maintaining grading infrastructures, overhauling labs, writing solution sheets.
Warblre --- Mechanized Semantics for JavaScript Regexes
Slides
Master thesis done at
System F, EPFL.
Supervised by Dr. Aurèle Barrière & Prof. Clément Pit-Claudel.
Ported the JavaScript regexes specification to the Coq proof assistant.
Care was taken to ensure that the ported specification was faithful to the original paper one, and that one could convince oneself of this fact.
Proved key properties of the specification, such as termination.
Additionally dis-proved some incorrect simplifications found in the literature about these semantics.
Exproc --- Computation Expressions for Scala
Repository
Semester project done at
LAMP, EPFL.
Supervised by Anatolii Kmetiuk.
Implemented an adaptation of F#'s computation expressions in Scala 3 using its meta-programming facilities.
Demonstrated how it could be used to make more natural and practical domain specific languages.
Implemented an interpreter for System F in the subset of Scala supported by Stainless, a verification tool for Scala.
Then proved the main properties of the implemented calculus, most notably that it satisfies progress and preservation.
This project used to be the second largest one (in number of verification conditions) done in Stainless.
It is also still used as a benchmark for Stainless, as part of the bolts repository.