@inproceedings{varatalu2025regex,
author = {Varatalu, Ian Erik and Veanes, Margus and Zhuchko, Ekaterina and Ernits, Juhan},
title = {Regex Decision Procedures in Extended RE#},
editor = {R. Piskac and Z. Rakamaric},
booktitle = {CAV 2025},
year = {2025},
month = {July},
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.},
publisher = {Springer},
url = {http://approjects.co.za/?big=en-us/research/publication/regex-decision-procedures-in-extended-re/},
pages = {106-129},
note = {Published in LNCS vol. 15933},
}