Formally Verified Matching of Regular Expressions
Abstract We demonstrate the benefit of computer assisted reasoning by proving correctness of some matching algorithms for regular expressions. We give a brief survey of the system used for verification, illustrate the problem, discuss the computation and usage of derivatives, present the machine assisted proofs and report on the effort for creating them.
Authors
- Christoph Walther (ORCID: https://orcid.org/0000-0002-9382-5399)
Institutions
- Darmstadt University of Applied Sciences (DE)
- Technische Universität Darmstadt (DE)
Publication Details
- Journal
- Journal of Automated Reasoning
- Published
- 2026-09-06
- DOI
- https://doi.org/10.1007/s10817-026-09761-0
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Technische Universität Darmstadt