Verified and Efficient Matching of Regular Expressions with Lookaround
summary
Presents a Coq formalization and a verified matcher that handles lookahead and lookbehind, including negative lookarounds via two complementary predicates, and extracts executable Haskell code. The algorithm decomposes expressions into layers (or-expressions on o-strings), uses marked regular expressions to simulate NFAs functionally, and resolves oracle queries bottom-up. Proof scripts total about 10,000 lines and experiments on worst-case patterns show runtime growing linearly in both regex size and input length. Claims and code are reproducible.
AI-written summary · about
chapters (13)
- 0:00Verified lookaround matching
- 1:07Lookaround semantics
- 3:38Lookaround properties
- 5:01Regex matching landscape
- 7:10Layer-wise matching algorithm
- 10:20O strings and oracle valuations
- 12:50Matching Orexs on O strings
- 14:16Implementation approaches
- 16:46Marked regex explained
- 19:14Verifying marked expressions
- 20:15Linear time complexity evaluation
- 21:40Key contributions summary
- 23:08Question and answer session
related talks
21mEfficient Matching of Regular Expressions with Lookaround Assertions
27mCertified hardware for regexp matching: A rocq library and its workflow
37mAll About Regular Expressions
01h 03mMatching Logic: Foundation of the K Framework
22mStatic Analysis for Checking the Disambiguation Robustness of Regular Expressions
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi
22mEREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
51mRegular Expressions in C++, Present and Future