Email Gateway (May 06 2026 at 16:07): Email Gateway (May 06 2026 at 16:07):From: Tobias Nipkow <nipkow@in.tum.de>
Aho-Corasick String Matching
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
This development formalizes the Aho-Corasick multi-pattern string matching
algorithm over lists. The verified executable reference automaton uses the
canonical Aho-Corasick state: after reading a text prefix, the state is the
longest suffix of that prefix that is also a pattern prefix. The development
also proves a state-only transition theorem, a fold-based scan invariant, and a
recursive failure-link transition refining the canonical transition, together
with equivalent state-carrying and failure-link search procedures. The main
theorem shows that the search procedure reports exactly the pattern occurrences
ending at each text position.
https://isa-afp.org/entries/Aho_Corasick.html
Enjoy!
Last updated: May 23 2026 at 03:31 UTC