Regex Decision Procedures in Extended RE#
Margus Veanes
Microsoft Research Redmond
Abstract:
We develop decision procedures for extended regular expressions in the
new ERE# framework that uses span semantics, utilizing the power of
symbolic derivatives. We prove a normal form theorem in Lean for ERE#
that is closed under all Boolean operations and provides the basis for
the given decision procedures. The tool is evaluated on existing SMT
benchmarks for regexes that shows it to be the fastest solver to date –
often orders of magnitude faster than state-of-the-art – albeit
specialized for the single-variable fragment of string theory.
Link to the paper:
Regex Decision Procedures in Extended RE# |
SpringerLink https://link.springer.com/chapter/10.1007/978-3-031-98682-6_7