4 papers
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…
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…
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…