Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
This provides foundational verification tools for JavaScript regular expressions, addressing correctness and optimization issues for developers and engine implementers.
The authors developed the first mechanized, proven-faithful semantics for JavaScript regular expressions with backtracking, capturing the full backtracking tree. They demonstrated its practicality by applying it to prove contextual equivalence for regex rewrites and formally verify the PikeVM algorithm used in real-world engines.
We present the first mechanized, succinct, practical, complete, and proven-faithful semantics for a modern regular expression language with backtracking semantics. We ensure its faithfulness by proving it equivalent to a preexisting line-by-line embedding of the official ECMAScript specification of JavaScript regular expressions. We demonstrate its practicality by presenting two real-world applications. First, a new notion of contextual equivalence for modern regular expressions, which we use to prove or disprove rewrites drawn from previous work. Second, the first formal proof of the PikeVM algorithm used in many real-world engines. In contrast with the specification and other formalization work, our semantics captures not only the top-priority match, but a full backtracking tree recording all possible matches and their respective priority. All our definitions and results have been mechanized in the Rocq proof assistant.