A Rocq-mechanized semantics for JavaScript regex with backtracking, proven equivalent to an ECMAScript embedding, then used to verify contextual equivalence of rewrites and to prove correctness of the PikeVM algorithm.
Proceedings of the ACM on Programming Languages 6, POPL (2022), 1–31
2 Pith papers cite this work, alongside 32 external citations. Polarity classification is still indexing.
2
Pith papers citing it
32
external citations · Crossref
representative citing papers
Generalization of Z3-Noodler's stabilization method to transducers enables efficient solving of relational string constraints and outperforms prior solvers by solving more instances orders of magnitude faster.
citing papers explorer
-
Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
A Rocq-mechanized semantics for JavaScript regex with backtracking, proven equivalent to an ECMAScript embedding, then used to verify contextual equivalence of rewrites and to prove correctness of the PikeVM algorithm.
-
String Solving with Stabilization and Transducers (Technical Report)
Generalization of Z3-Noodler's stabilization method to transducers enables efficient solving of relational string constraints and outperforms prior solvers by solving more instances orders of magnitude faster.