Lean Formalization of Extended Regular Expression Matching with Lookarounds

Explore a 28-minute conference talk from CPP 2024 that delves into the Lean formalization of extended regular expression matching with lookarounds. Learn about an algorithm for matching extended regular expressions based on locations and symbolic derivatives, supporting intersection, complement, and lookarounds. Discover how this implementation mirrors an extension of the .NET NonBacktracking regular expression engine. Understand the formalization process using the Lean 4 proof assistant and the proof of correctness with respect to standard matching semantics. Gain insights from researchers Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner as they present their work on this advanced topic in regular expression matching and formal verification.