Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics(…)
summary
Paper presents a mechanized, ECMAScript‑faithful semantics for JavaScript regexes in the Rocq proof assistant, equating a concise 21 inductive rules semantics with a prior line‑by‑line Warbler mechanization. It defines a backtracking tree that records all match paths and uses it to give a contextual equivalence (match‑leaf equality) and to verify an NFA‑based PikeVM algorithm including a corrected progress check; proofs and reusable artifacts are mechanized and available.
AI-written summary · about
chapters (10)
- 0:00Formal verification intro
- 1:46Modern vs traditional regex
- 3:33Regex semantics challenges
- 7:24Backtracking trees foundation
- 10:16Semantic rules for features
- 13:02Regex equivalence formalized
- 16:12Verifying regex optimizations
- 16:56PVM matching correctness
- 20:50Future for verified engines
- 22:15Q&A
related talks
23mLinear Matching of JavaScript Regular Expressions
01h 06mEverybody stands back! I know regular expressions
29mReimplement RegExp in JavaScript
15mTowards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal"
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi
22mTwo Problems: Regular Expressions for Revolutionaries
01h 13m/ Reg (exp) {2} lained / Demystifying Regular Expressions
17mWhen Chomsky Met JavaScript: Exploring the Linguistics(...)