26 citations · 26 across the 3 of their papers we have counts for
5 papers · 1 filter
On the computational complexity of JavaScript regex matching
Victor Deng, Aurèle Barrière, Clément Pit-Claudel
Despite widespread use, the complexity class of modern regular expression matching was not well-understood. Previous work proved that regular expression matching with backreference…
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
Aurèle Barrière, Victor Deng, Clément Pit-Claudel
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its fa…
A Coq Mechanization of JavaScript Regular Expression Semantics
Noé De Santo, Aurèle Barrière, Clément Pit-Claudel
We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition…
Linear Matching of JavaScript Regular Expressions
Aurèle Barrière, Clément Pit-Claudel
Modern regex languages have strayed far from well-understood traditional regular expressions: they include features that fundamentally transform the matching problem. In exchange f…
Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière, Sandrine Blazy, David Pichardie
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution,…