Beyond Classical Regexes: Symbolic-Derivative-Based Decision Procedures for Extended Regular Expressions
Talk by Margus Veanes
Abstract: Regular-expression derivatives are a classic tool with modern relevance: they yield compact, compositional algorithms for matching and equivalence. When regular expressions are extended with additional operators, however, derivative computation must be redesigned to remain sound, terminating, and useful in practice. This talk surveys recent algorithmic extensions in this space, centered on ERE# (CAV’25) and the forthcoming EREQ (PLDI’26) extension that embeds weak MSO. I will explain the key semantic choices behind these formalisms, how they impact derivative rules, and how normalization/canonicalization enables effective reasoning despite increased expressiveness. The goal is to convey a unified perspective on how to extend derivative-based methods without losing their algorithmic advantages.
Bio: Margus Veanes is a principal researcher at Microsoft Research Redmond. His current research agenda is to develop scalable analysis techniques and corresponding logical foundations for analysis of programs manipulating strings. He is also investigating foundations for behavioral model analysis in the context of model validation and model-based testing. The main focus is on the use of symbolic automata theory in combination with state-of-the-art satisfiability modulo theories techniques. He is a co-designer and co-developer of Spec Explorer 2004, and a co-author of the book Model-Based Software Testing and Analysis with C.
