一句话：提出基于导数的非回溯正则匹配算法，支持锚点与计数并保持回溯语义，已在 .NET 7 实现并形式验证。
针对传统回溯正则引擎在最坏情况下可能指数级超时，而现有非回溯引擎又难以兼容回溯语义的问题，本文提出基于导数的非回溯正则匹配理论与算法。该算法支持锚点与计数，保持回溯语义，并可扩展 lookaround。作者给出算法正确性的形式化证明，并描述以正则重写系统为核心的实现。该实现作为 .NET 的新正则后端，随 .NET 7 正式发布过程经过广泛测试；论文还在工业案例与其他正则引擎上进行了综合评估。
We develop a new derivative based theory and algorithm for nonbacktracking regex matching that supports anchors and counting, preserves backtracking semantics, and can be extended with lookarounds. The algorithm has been implemented as a new regex backend in .NET and was extensively tested as part of the formal release process of .NET7. We present a formal proof of the correctness of the algorithm, which we believe to be the first of its kind concerning industrial implementations of regex matchers. The paper describes the complete foundation, the matching algorithm, and key aspects of the implementation involving a regex rewrite system, as well as a comprehensive evaluation over industrial case studies and other regex engines.
@article{paperbot1996,
title = {Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics},
author = {Dan Moseley and Mario Nishio and Jose Perez Rodriguez and Olli Saarikivi and Stephen Toub and Margus Veanes and Tiki Wan and Eric Xu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591262}
}