Formally verified matching of regular expressions

DOI10.1007/S10817-026-09761-0MaRDI QIDQ7405771zbMATH OpenFDO

Authors Christoph Walther

Publication date 2026

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-026-09761-0

zbMATH Keywords

automated reasoningderivativesprogram verificationregular expressionstheorem proving by inductionVeriFun

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Compact Proof of Decidability for Regular Expression Equivalence
• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Certified parsing of regular languages
• Derivatives of Regular Expressions
• EDUCATIONAL PEARL: ‘Proof-directed debugging’ revisited for a first-order version
• Fermat, Euler, Wilson -- three case studies in number theory
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• On proving the termination of algorithms by machine
• Partial derivatives of regular expressions and finite automaton constructions
• POSIX lexing with derivatives of regular expressions
• Programming Techniques: Regular expression search algorithm
• Proof Pearl: regular expression equivalence and relation algebra
• Proof-directed debugging
• Reasoning about incompletely defined programs
• Regular-expression derivatives re-examined
• Unified decision procedures for regular expression equivalence
• Verified Newton-Raphson iteration for multiplicative inverses modulo powers of any base

This page was built for publication: Formally verified matching of regular expressions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7405771)