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 VeriFun 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. 1 Introduction Regular expressions provide an elegant way to define regular languages and have motivated researches from the reasoning community to verify algorithms working on regular expression. To solve the matching problem for a word w and a regular expression r means to decide whether w is an element of the language \(\mathcal {L}(r)\) defined by r. The matching problem can be solved by transforming r to a deterministic finite automaton dfa(r) which (by construction) accepts only the words in \(\mathcal {L}(r)\), see e.g. [11]. As an alternative approach, Harper developed an algorithm which solves the matching problem directly, i.e. without the detour of creating a dfa in a preprocessing step [10]. The motivation of this work was to illustrate the interplay between programming and proving in the development of a program when teaching students to reason inductively in an introductory programming course. As Harper’s method uses higher-order functions as well as a continuation-passing style, Yi reformulated the method in first-order logic plus induction to make it more accessible for students in the class room [27]. He also provided hand-crafted correctness proofs which is particularly important as the solution for the matching problem is rather tricky and its correctness is far from being obvious. We use a proof assistant here as computer assisted proofs increase the confidence in the correctness of a program because not only programs or their specification may be erroneous, but also faults may have crept into a hand-written correctness proof or are hidden in the gaps usually present in manual proofs, see [21] for an example. Also a manual correctness proof of a non-simple program (like the matching algorithms considered here) with the needed rigor may become a Sisyphean task by the sheer quantity of the required details and proof steps. Subsequently we demonstrate the use of a proof assistant for proving correctness of the matching algorithm formulated in [27] and compare with verification of a matching algorithm published some time ago [4]. 2 eriFun The formal proofs presented here are performed with the \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) system [19].Footnote 1 This system was designed and developed as an easy to learn and easy to use tool for teaching Automated Reasoning, Semantics, Verification and similar subjects. The system provides a high degree of automatization thus relieving a user from routine proof steps, and has been used in beginner courses about Formal Methods as well as in practical courses about Program Verification for about 15 years [24]. \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) ’s object language consists of principles for defining polymorphic data types, procedures operating on them, and for statements (called “lemmas”) about the data types and procedures. The language allows Unicode and offers in-, out-, pre- and postfix notation so that readability is increased by use of the familiar mathematical notation. Infix operators also carry a precedence which we omit in our examples for sake of simplicity. Figure 1 displays some examples used in this case study. The data type \(\textsf{bool}\) and the data type \( \mathbb {N}\) for natural numbers built with the constructors 0 and \(\phantom {a}^{\texttt {+}} \texttt {(}\ldots \texttt {)}\) for the successor function are the only predefined data types in the system. \(\phantom {a}^{{\texttt {-}}} \texttt {(}\ldots \texttt {)}\) is the selector of \(\phantom {a}^{\texttt {+}} \texttt {(}\ldots \texttt {)}\) thus denoting the predecessor function. Data type \(\textsf{list}\) is user defined and represents linear lists. Identifiers preceded by @ denote type variables, and therefore polymorphic lists are defined here. Lists are built with the constructors ø for the empty list and :: (given in infix-notation). The functions \(\textsf{hd}\) and \(\textsf{tl}\) (for head and tail) are the selectors of :: yielding—if applied to a non-empty list—the leftmost list element and the list with the leftmost list element removed respectively. Selectors applied to constructors they do not belong to as e.g. \(\phantom {a}^{{\texttt {-}}} \texttt {(}0{\texttt {)}}\), \(\textsf{hd}\)(\(\o \)) and \(\textsf{tl}\)(\(\o \)) remain unevaluated and denote an unknown value of appropriate type, see [23]. Procedures are defined by \(\textsf{if}\)- and \(\textsf{case}\)-conditionals, functional composition and recursion. Procedure calls are evaluated eagerly, i.e. call-by-value. Predicates are defined by procedures with result type \(\textsf{bool}\). Procedure \(\mathsf {\subseteq }\) of Fig. 1 is an example of a predicate used in this case study. It decides the sublist relation without respecting the order and multiple occurrences of list elements, as e.g. \(2\,\)::\(\,1\,\,\)::\(\,1\,\):: ø \(\subseteq 1\,\)::\(\,2\,\):: ø and vice versa. Upon the definition of a procedure, \(\left. {{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}'\textrm{s}\right. \) automated termination analysis (based on the method of Argument-Bounded Functions [20, 25] ) is invoked for generating termination hypotheses which are sufficient for the procedure’s termination and proved like lemmas. If termination analysis fails, the user has to provide a termination function for generating termination hypotheses. Afterwards induction axioms are computed from the terminating procedures’ recursion structures to be on stock for future use. Procedures can be tested by running them in the system’s Interpreter, thus supporting program development. Lemmas are defined with the conditional \(\textsf{if}\) : \(\mathsf {bool\times bool\times bool\rightarrow bool}\) and negation \(\lnot \) as connectives. One writes e.g. \(\textit{if}\{a,b,\textit{true}\}\) for \( a\rightarrow b\), \(\textit{if}\{a,b,\textit{false}\}\) for \(\left. a\wedge b\right. \), \(\textit{if}\{a,\textit{true},b\}\) for \(a\vee b\) etc. Connective \(\lnot \) is formally not required and used to avoid clumsy expressions of form \(\textit{if}\{a,\textit{false},\textit{true}\}\). Only universal quantification is allowed for the variables of a lemma. Fig. 1 displays a lemma about list membership \(\in \) and \(\subseteq \) which is frequently used in subsequent proofs. The string in the headline (between “lemma” and “ < =”) is just an identifier assigning a name to the lemma for reference and must not be confused with the statement of the lemma given as a boolean term in the lemma body. See [23] for a more detailed account of the system’s object language. Subsequently, lemmas and proof obligations will be written in the usual mathematical notation. Lemmas are proved with the HPL-calculus (abbreviating Hypotheses, Programs and Lemmas) [24]. The most relevant proof rules of this calculus are Induction, Use Lemma, Apply Equation, Unfold Procedure, Case Analysis and Simplification. A deduction in the HPL-calculus is represented by a tree whose nodes are sequents. Sequents are expressions of form \(\langle H,\textit{IH} \vdash goal \rangle \), where H is a finite set of hypotheses given as literals, i.e. negated or unnegated if-free boolean terms, \(\textit{IH}\) is a finite set of induction hypotheses given as possibly quantified boolean terms and goal is a boolean term, called the goalterm of the sequent. A sequent stands for the closed formula with universally quantified non-induction variables in the induction hypotheses. The sequent \(\langle \emptyset ,\emptyset \vdash \textit{body}\rangle \) is the root node of the proof tree of a lemma \(\ell \) with body \(\textit{body}\). A lemma \(\ell \) is developed iff goal equals \(\textit{true}\) for each sequent at a leaf of the proof tree associated with \(\ell \), and is verified if additionally each lemma applied by Use Lemma or Apply Equation when building the proof tree is verified. By choosing Simplification for some leaf of the proof tree, the system’s first-order theorem prover, called the Symbolic Evaluator, is started for rewriting the leaf’s goalterm using the definitions of the data types and procedures, the leaf’s hypotheses and induction hypotheses as well as the lemmas already verified. This reasoner is guided by heuristics, e.g. for deciding whether to unfold a procedure call, to use a lemma and for speeding up proof search by filtering out useless lemmas. Equality reasoning is implemented by conditional term rewriting with ACI-matching, where the orientation of equations is heuristically established. The Symbolic Evaluator is a fully automated tool over which the user has no control, thus leaving the HPL-proof rules as the only means to guide the system to a proof. Also the HPL-calculus is controlled by heuristics. By applying the Verify command to a lemma, the system starts to compute a proof tree by choosing appropriate HPL-proof rules heuristically. If a proof attempt gets stuck, the user must step in by applying a proof rule to the goalterm of some leaf of the proof tree (sometimes after pruning some unwanted branch of the tree), and the system then takes over control again. Also it may happen that a fresh lemma must be formulated before the proof under consideration can be completed. All interactions are menu driven so that typing in proof scripts is avoided. The system also provides a Disprover [1] which is useful for testing a lemma before a proof attempt is started. \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) is implemented in Java and installers for running the system under Windows, Unix/Linux or Mac are available from the web [19]. When working with the system, we use proof libraries which had been set up over the years by extending them with definitions and lemmas being of general interest. When importing a definition or a lemma from a library into a case study, all program elements and proofs on which the imported program element depends are imported as well. E.g., the correctness proof for the matching algorithm from [27] depend on 1 procedure and 7 lemmas from our Arithmetic-library and on 4 procedures and 16 lemmas from our List-library. In the sequel, we will only present the lemmas which are essential to understand the proofs and refer to [19] for a complete account of all used lemmas and their proofs. 3 Syntax and Semantics of Regular Expressions Figure 2 displays the definitions of the basic notions: Our alphabet \(\Sigma \) consists of letters \(a(0),a(1),a(2),\ldots \) and \(\Sigma ^{*}\) denotes the set of words which are obtained by adding letters from \(\Sigma \) iteratively with the word constructor \(\cdot \) to the empty word \(\mathsf {\varepsilon }\). Data type \(\textsf{RegExp}\) defines the syntax of regular expressions with the alternative operator \(\mid \), the sequence operator \(\odot \) and the Kleene-star \(\mathsf {*}\). The operator for the empty word is given by \(\epsilon \) and \(\mathfrak {c}\) is a type conversion operator which converts letters to regular expressions. The semantics of a regular expression r is given by a language \(\mathcal {L}(r)\subset \Sigma ^{*}\), i.e. a potentially infinite set of words defined by where \(\mathcal {L}(r_{1})\otimes \mathcal {L}(r_{2})\) denotes the concatenation of languages, i.e. the smallest set of words containing \(u\circ v\) for each \(u\in \mathcal {L}(r_{1})\) and each \(v\in \mathcal {L}(r_{2})\) and \(\circ \) stands for the concatenation of words. The language \(\mathcal {L}_{n}\) is defined by \(\mathcal {L}_{0}(r):=\{\mathsf {\varepsilon } \}\) and \(\mathcal {L}_{n+1}(r):=\mathcal {L} (r)\otimes \mathcal {L}_{n}(r)\cup \{\mathsf {\varepsilon }\}\) for each \(n\in \mathbb {N}\). Language \(\mathcal {L}(r)\) is formally defined by procedure £ of Fig. 3 (where procedure \(\textit{function}\) \([\textit{infixr}]\) \(<>(k,l\):\(\textit{list}[@T])\):\(\textit{list}[@T]\) \(<=\ldots \) computes list concatenation): For each \(n\in \mathbb {N}\), we define £(r, n) as \(\mathcal {L}(r)\) if r is formed with an operator different from \(*\) and we define £\((r^{*},n)\) as \(\mathcal {L}_{n}(r)\). Then \(w\in \mathcal {L}(r)\) iff \(w\in ~\)£(r, n) for some \(n\in \mathbb {N}\). Moreover, as the required iterations of the Kleene-star are bounded above by the length \(\left| w\right| \) of the word w under consideration, we find \(w\in \mathcal {L}(r)\) iff \(w\in ~\)£\((r,{\left| w\right| })\). We use lists of words when defining £ in the system’s object language and use notions and lemmas from our List-library upon program development and verification. Procedure \(\pounds ^{*}\) of Fig. 3 computes the union of the languages of the regular expressions in list R. Procedure \(\pounds ^{*}\) is needed to specify soundness and completeness of the matching algorithm from [27] as this algorithm requires a list of regular expressions as input instead of a single one. The following lemmas about £ and \(\pounds ^{*}\) are subsequently required: where procedure \(\textit{function}\) \([\textit{infix}]\) \(\circledcirc (R\):\(\textit{list}[\textit{RegExp}],r\):\(\textit{RegExp})\):\(\textit{list} [\textit{RegExp}]\) \(<=\ldots \) computes the smallest list of regular expressions containing \(r^{\prime }\odot r\) for each member \(r^{\prime }\) of R. For proving (1)–(3), the following lemmas about language concatenation have been used: \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) proves the lemmas (2 )–(7) automatically and also orients the equations in these lemmas left-to-right, thus supporting subsequent equality reasoning. The lemmas (1) and (8) need one hint each (i.e. a user initiated HPL-proof rule application) to complete the proofs. 4 The Matching Algorithm Regular expressions r provide an inherent non-determinism which must be resolved when attempting to match a word w with r. This non-determinism stems from the presence of alternatives, either given explicitly by the alternative-operator \(\mid \) or implicitly by the Kleene-star, because \(r^{*}\) stands for an infinite sequence \(\epsilon ,\) r, \(\left. r\odot r,\right. r\odot r\odot r,\) \(\ldots \) of alternatives. The non-determinism given by \(\mid \) is easily resolved as there are only finitely many alternatives to inspect. The non-determinism coming with \(*\) can be resolved by an 1-letter lookahead organized in a depth-first search manner. We illustrate this by an example: Let us try to match the word abaaba with the regular expression \(({\textsf {ab}}\mid {\textsf {a}})^{\mathsf {*}}\) aba by scanning the word letter by letter. We have 3 options to start with, viz. match abaaba with (1) aba as \(\varepsilon \) matches \((\mathsf {\ldots })^{\mathsf {*}} \), with (2) ab(ab\(\mathsf {\mid }{\textsf {a}})^{*}\) aba or with (3) a(\({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba. Alternative (1) fails as aba remains after trying to match abaaba with aba, hence we continue with trying to match aaba with (2.1) aba, with (2.2) ab(\({\textsf {ab}}\mathsf {\mid }{\textsf {a}})^{*}\) aba or with (2.3) a(ab\(\mid \) a\()^{*}\) aba. Alternative (2.1) fails because aba does not match ba, alternative (2.2) fails as well as aba does not match b(ab\(\mathsf {\mid }{\textsf {a}})^{*}\) aba, hence we are left with matching aba with \(({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba. This provides us with 3 choices again: Match aba with (2.3.1) aba, with (2.3.2) ab(\({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba or with (2.3.3) a(\({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba. As aba matches (2.3.1) aba, the match of abaaba with (\({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba is established. This search is implemented by procedure \({\dag }\) displayed in Fig. 4, which has been obtained from the rule system presented in Fig. 1 of [27]. Upon matching a word with first letter c with a regular expression r, procedure \({\dag }\) computes a list of regular expressions representing the alternatives which have to be explored. For the example above, a call of \((({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba \({\dag }\) a) yields list ba :: \({\textsf {b}}({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba :: \(\epsilon ({\textsf {ab}}\mid {\textsf {a}})^{*}\) aba ::ø as result. Using procedure \({\dag }\), the matching algorithm ! can be formulated. This procedure is obtained from the rule system presented in Fig. 1 of [27] and is displayed in Fig. 6. A naive approach to match some \(w\in \Sigma ^{*}\) with a regular expression \(r_{1}\odot r_{2}\) would be to match some prefix u of w with \(r_{1}\) and afterwards try to match the remaining suffix v (which has not been consumed upon matching of w with \(r_{1}\)) with \(r_{2}\). But matching v with \(r_{2}\) may fail as different separations u, v of w may exist, and backtracking is needed then. However, backtracking is avoided if \(r_{1}=\epsilon \), \(r_{1}=\mathfrak {c}(\ldots )\) or \(r_{1}=(\ldots )^{*}\) as v is known a priori in these cases, viz. \(v=w\) or \(v=\textit{rest}(w)\) in the latter cases. Therefore the matching algorithm ! rearranges a regular expression of form \(r_{1}\odot r_{2}\) recursively upon matching until \(r_{1}=\epsilon \), \(r_{1}=\mathfrak {c} (\ldots )\) or \(r_{1}=(\ldots )^{*}\), where procedure \({\dag }\) is called if \(r_{1}=(\ldots )^{*}\). 4.1 Correctness of Procedure \({\dagger }\) The soundness requirement for procedure \({\dagger }\) (displayed in Fig. 4) is given by where the right-context K is not required to express soundness, but is needed in subsequent proofs. Using the lemmas presented in Sect. 3, the system proves soundness lemma (9) by induction based on the recursion structure of procedure \({\dag }\) yielding 3 base and 6 step cases. Five hints for using an HPL-proof rule are required to complete the proofs of 2 of the step cases. The remaining 7 cases are proved automatically. Completeness of procedure \({\dag }\) is stipulated by lemma \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) starts an induction based on the recursion structure of procedure \({\dag }\) and automatically succeeds for all cases, except when (a) \(r=\mathfrak {c}(\textit{letter}(\textit{prefx}(r)))\odot \textit{suffx}(r)\), (b) \(r=\textit{arg}(\textit{prefx}(r))^{*}\odot \textit{suffx}(r)\) or (c) \(r=\textit{arg}(r)^{*}\). Case (a) is easily solved by instructing the system to use an auxiliary lemma, but both remaining proofs turn out to be the most challenging in the whole case study as they require several user interactions. Also non-trivial lemmas have to be spotted from the proof obligations on which the system gets stuck. We illustrate the proof for case (c) in some detail. Having crafted a proof for this case, the proof for case (b) is obtained by similar reasoning. When attempting to prove (10) for \(r=\textit{arg} (r)^{*}\), the system halts with proof obligation As \(w\in \ \)£\((\textit{arg}(r),n)\,\otimes \) £\((r,n-1)\), some \(u\in \ \)£\((\textit{arg} (r),n)\) and some \(v\in \) £\((r,n-1)\) exist such that \(w=\left. u\circ v\right. \). If \(u\in \mathcal {L}(r)\) and \(v\in \mathcal {L}(r^{*})\), then \(\mathcal {L}(r)\ne \{\varepsilon \}\) as otherwise \(\mathcal {L}(r^{*})=\{\varepsilon \}\) and then \(w=\varepsilon \circ \varepsilon \) contradicting \(w\ne \varepsilon \). Consequently \(u\ne \varepsilon \) for some \(u\in ~\)£\((\textit{arg}(r),n)\), hence (i) \(\textit{first} (w)=\textit{first}(u)\) and (ii) \(\textit{rest}(w)=\textit{rest} (u)\circ v\). We obtain \(\textit{rest}(u)\in ~{\pounds }^{*}(\textit{arg} (r)\,\dag \textit{first}(u),n)\) by the induction hypothesis and therefore \(\textit{rest} (u)\circ v\in ~{\pounds }^{*}(\textit{arg}(r)\,\dag \,\textit{first} (u),n)~\otimes ~{\pounds }(r,\left. n-1)\right. \). Consequently \(\textit{rest} (w)\in ~{\pounds }^{*}(\textit{arg}(r)\,\dag \,\textit{first}(w),n)~\otimes ~{\pounds }(r,n-1)\) by (i) and (ii), then \(\textit{rest}(w)\in ~{\pounds }^{*}(\textit{arg}(r){{\dag }}\,\textit{first} (w),n)~\otimes ~{\pounds }(r,n)\) by lemmata (1) and (8), and proof obligation (11) is verified. To teach \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) this proof idea, we first have to stipulate how a word \(w\ne \varepsilon \) is separated into words \(u\ne \varepsilon \) and v such that \(w=u\circ v\). To this effect we define two procedures \(\textsf{U}\) and \(\textsf{V}\) which are displayed in Fig. 5, where procedure \(\textit{function}\) \([\textit{infixr}]\) \(\lhd (w\):\(\Sigma ^{*} ,L\):\(\textit{list}[\Sigma ^{*}])\):\(\textit{list}[\Sigma ^{*}]\) \(<=\ldots \) computes the smallest list of words containing \(w\circ \ell \) for each \(\ell \in L\). Procedures \(\textsf{U}\) and \(\textsf{V}\) are incompletely defined as no results are stipulated if \(w\notin (L\backslash \hspace{-0.08cm}\backslash \varepsilon )\otimes K\), where procedure \(\textit{function}\) \([\textit{infix}^{*}]\) \(\backslash \hspace{-0.08cm}\backslash (k\):\(\textit{list}[@T],i\):@T):\(\textit{list}[@T]\) \(<=\ldots \) removes each occurrence of i from list k. This means that calls of \(\textsf{U}\) and \(\textsf{V}\) denote unspecified words in this case.Footnote 2 For verifying proof obligation (11), the following lemmas about \(\textsf{U}\) and \(\textsf{V}\) are needed: Additionally we have to make the system aware of the fact that \(\mathcal {L}(r^{*})\ne \{\varepsilon \}\) entails \(\mathcal {L} (r)\ne \{\varepsilon \}\). This is achieved by formulating the lemmaFootnote 3 \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) orients the equations in (14) and (15) left-to-right and proves the lemmas (12)–(15) automatically by induction upon the recursion structure of the procedures \(\textsf{U}\) and \(\textsf{V}\) respectively. The induction proof of lemma (16) (based on the recursion structure of procedure £) needs some support by prompting the system to use two case analyses, a lemma and an induction hypothesis. Now the proof of the completeness statement (10) can be finished, however with much user support. In a first step, we interactively use lemma (14) with HPL-rule Apply Equation to replace \(\textit{rest}(w)\) in proof obligation (11) with and subsequently have to provide the system with 8 further hints to complete the proof for case (c) \(r=\textit{arg}(r)^{*}\). Another 11 hints are needed to finish the proof for case (b) \(r=\textit{arg} (\textit{prefx}(r))^{*}\odot \textit{suffx}(r)\). 4.2 Correctness of Procedure ! The soundness requirement for procedure ! (see Fig. 6) is formulated by and the completeness statement is given as Using the lemmas presented in the previous sections, \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) proves both theorems by induction based on the recursion structure of procedure ! yielding 3 base and 10 step formulas for each of the proofs. The system automatically succeeds for 11 cases and must only be supported with 5 user hints to complete the proof of both remaining cases when proving soundness (17). The proof of completeness (18) necessitates even less interaction, as only 4 hints are required for 2 of the 13 cases to guide the system to success. 5 Derivatives Many years ago, Brzozowski introduced the notion of derivatives of regular expressions [4]: Given a letter c and a regular expression r, the derivative \(\eth _{c}\mathbb {(}r\mathbb {)} \) of c and r is a regular expression satisfying \(u\in \mathcal {L} (\eth _{c}\mathbb {(}r\mathbb {)})\) iff \(c\cdot u\in \mathcal {L} (r)\). The definition of \(\eth \) requires an additional regular operator for the empty language, \(\varnothing \) say, so that e.g. \(\eth _{c}\mathbb {(}\epsilon )=\varnothing \) can be defined. Fig. 7 displays procedure \(\eth \) for computing derivatives based on the rule system presented in [4], where procedure \(\mathcal {E}\) decides whether \(\varepsilon \in \pounds (r,n)\) as proven with \(\forall r\):\(\textit{RegExp} ,n\):\(\mathbb {N} \, \mathcal {E(}r)\leftrightarrow \varepsilon \in \pounds (r,n)\). Soundness and completeness of procedure \(\mathbb {\eth }\) is expressed like for procedure \({\dag }\), where the procedure calls \({\pounds }^{*}(r\,\)† \(\textit{first}(w))\) in the lemmas (9) and (10) are replaced with \(\pounds (\mathbb {\eth (}r,\textit{first}(w)))\). The proofs of the modified lemmas (\(9^{\prime }\)) and (\(10^{\prime }\)) are similar to the proofs for \({\dag }\). While the motivation for introducing derivatives was mainly to provide a technique for compiling regular expressions to deterministic finite automatons (which additionally supports the extension of regular expression with boolean operators) [15], Brzozowski also presented a method for regular expression matching based on derivatives [4, 17] . Procedure \(\textsf{drvs}\)-\(\eth \) of Fig. 7 iteratively computes all derivatives of an input word w which are joined with the alternative operator \(\mid \) to a single regular expression. A successful match of w with r is established iff \(\mathcal {E(}r^{\prime })\) holds for some of the \(\mid \) - components of \(\textsf{drvs}\)- \(\eth (r,w)\). Soundness of the method is expressed by which (using Lemma (\(9^{\prime }\))) is automatically proved. The proof of the completeness statement uses Lemma (\(10^{\prime }\)) and needs one hint to use the induction hypothesis. Compared with matching algorithm !, the correctness proof of Brzozowski’s method requires less effort for the user as well as for the system, but is rather inefficient. For instance, \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\)’s interpreterneeds 1858 steps to confirm that abaaba matches \(({\textsf {ab}}\mid {\textsf {a}})^{\mathsf {*}}{\textsf {aba}}\) when using Brzozowski’s method, whereas procedure ! requires 330 steps only. Mismatches are represented by regular expressions involving \(\varnothing \). In the example, \(\textsf{drvs}\)-\(\eth \) computes a regular expression with 12 \(\mid \) - components where 10 of them are of form \(\varnothing \) or \(\varnothing \odot r\) so that \(\mathcal {E}\) computes \(\textit{false}\) for them. An alternative is to get rid of the regular operator \(\varnothing \) and to use lists \(\mathbb {\partial }_{c}\mathbb {(}r\mathbb {)}\) of derivatives instead. This yields the modified requirement \(u\in \bigcup \nolimits _{r^{\prime }\in \mathbb {\partial }_{c}\mathbb {(}r\mathbb {)} }\mathcal {L} (r^{\prime })\) iff \(c\cdot u\in \mathcal {L} (r)\), where e.g. \(\mathbb {\partial }_{c}\mathbb {(}\epsilon )=\) ø now is defined, see Fig. 8. The regular expressions in \(\mathbb {\partial }_{c}\mathbb {(}r\mathbb {)}\) are known as Antimirov derivatives [2]. Soundness and completeness of procedure \(\mathbb {\partial }\) is expressed like for procedure \({\dag }\), where the procedure calls \((r\,\)† \(\textit{first}(w))\) in the lemmas (9) and (10) are replaced with \(\mathbb {\partial (} r,\textit{first}(w))\). The proofs for \(\mathbb {\partial }\) are similar to the proofs for \({\dag }\), where the soundness proof needs 4 user hints and the completeness proof requires 18 user interventions to guide the system to success. Procedure \(\textsf{drvs}\)-\(\partial \) of Fig. 8 iteratively computes all Antimirov derivatives wrt. the letters of an input string. Matching of a word w with a regular expression r succeeds iff \(\mathcal {E}^{*}\mathcal {(} \textsf{drvs}\)-\(\partial (r\,\)::\(\,{\o },w))\) holds, where procedure \(\textit{function}\) \(\mathcal {E}^{*}(R\):list\(\textit{[}\) RegExp ]):\(\textit{bool}\) \(<=\ldots \) decides whether \(\mathcal {E}(r)\) holds for some \(r\in R\). Soundness of procedure \(\textsf{drvs}\)-\(\partial \) is expressed by Having helped the system with one hint to prove auxiliary lemma the proof for the soundness statement (21) is automatically computed. The completeness statement for \(\textsf{drvs} \)-\(\partial \) is given by which needs an auxiliary lemma too. One user hint is required to find the proof for lemma (24), and then the completeness statement (23) is proved with one user hint as well. Brzozowski-matching with Antimirov derivatives is more efficient than with Brzozowski derivatives for our example, as the system’s interpreter needs 1411 steps only. A reason might be that Brzozowski derivatives of form \(\varnothing ,\varnothing \odot r\) or \(r\odot \varnothing \) simply disappear because procedure \(\partial \) computes the empty list ø for them and \(\left. {\o }\,<>\ell \right. =\left. \ell <>\,{\o }\right. =\ell \). But nevertheless the number of steps is increased by a factor \(>4\) compared to matching procedure !. There are two reasons for this effect: First, procedure \({\dag }\) computes derivatives as well, but the computation of Antimirov derivatives by procedure \(\partial \) differs from the computation of Yi derivatives by procedure \({\dag }\) for regular expressions of form \(r_{1}\odot r_{2}\) (and coincides for all other cases). Table 1 displays the differences, where “\(\Rightarrow \ldots \)” gives the final result for Antimirov derivatives after subsequent computations if \(r_{1}\) is non-recursive. These final results coincide with the respective Yi derivatives, except for case (2) with the redundant regular expression \(\epsilon \odot r\) instead of r. Subsequent computations are required in all cases by the calls of procedures \(\mathcal {E}\) and \(\circledcirc \) which are not needed upon computation of Yi derivatives, except for \(\circledcirc \) in case (6) for the Kleene-star. As a consequence for our example, the system’s interpreter computes a list of 4 Antimirov derivatives within 1336 steps when using procedure \(\left. \textsf{drvs}{\textsf {-}}\partial \right. \) whereas the effort is reduced by a factor \(>5\) when procedure \({\dag }\) is (iteratively) used because (another) list of 4 regular expressions is computed within 230 steps only. Yi derivatives are not necessarily identical with Antimirov derivatives but are equivalent, i.e. \(\bigcup \nolimits _{r^{\prime }\in (r\,{\dag }\,c)}\mathcal {L} (r^{\prime } )=\bigcup \nolimits _{r^{\prime }\in \mathbb {\partial }_{c}\mathbb {(}r\mathbb {)} }\mathcal {L} (r^{\prime })\), as proven with The second cause for runtime improvement is that derivatives are computed for each regular expression encountered upon Brzozowski-matching. In contrast, procedure ! uses derivatives only for regular expressions formed with the Kleene-star and processes all other regular operators directly. The upper four rows of Table 2 shows for our example that Yi-matching always outperforms Brzozowski-matching independent of whether Yi derivatives or Antimirov derivatives are used. The methods for computing derivatives by procedure \({\dag }\) and for deciding the word problem by procedure ! can be modified yielding the procedures \({\dag \dag }\) and !! of Fig. 9: Procedure \({\dag \dag }\) computes derivatives as a regular expression (instead of a list of regular expressions) and procedure !! uses a regular expression (instead of a list of regular expressions) as argument for matching. Soundness and completeness of procedure !! is proved like for procedure ! and equivalence of Brzozowski derivatives with the derivatives computed by procedure \({\dag \dag }\) is proven similar to Theorem 25. As illustrated above, less costly computations result when deciding the word problem and upon synthesis of derivatives by the modified procedures !! and \({\dag \dag }\) than with the procedures \(\textsf{drvs}\)-\(\eth \) and \(\eth \) of Fig. 7. The modified matcher !! even outperforms Yi’s original matcher ! and is almost 9 times faster for our example than Brzozowski’s original matcher as displayed in the two bottom rows of Table 2. Hence one might consider the procedures !! and \({\dag \dag }\) as a more efficient alternative to Brzozowski’s matcher \(\mathcal {E\circ \,}\textsf{drvs}\)-\(\eth \) and Brzozowski derivatives computed with procedure \(\eth \) which are used quite often in other works, see Section 6. 6 Related Work Regular expressions have attracted developers and users of proof systems to verify correctness of algorithms working on regular expressions: Correctness of Brzozowski’s matcher \(\mathcal {E\circ \,}\textsf{drvs}\)-\(\eth \) of Fig. 7 has been verified with Coq in [6], with Isabelle/HOL in [12], and with Agda in [16] among others. Using Brzozowski derivatives, a simple procedure for deciding equivalence of regular expressions is developed in [12] and partial correctness is verified with Isabelle/HOL. It is demonstrated in addition how equivalence of regular expressions is used to prove (in)equalities in relational algebras. In [6] a decision procedure for regular expression equivalence using Brzozowski derivatives is developed as well and total correctness is proven with the Coq system. The paper also discusses the encoding of finite sets in type theory. A different approach for deciding equivalence is taken in [3]: The method uses pointed (also called marked) regular expressions instead of derivatives. This avoids quotient derivatives relative to an equivalence relation on regular expression which is required to get a finite number of states for a finite automaton when using derivatives. Correctness of the equivalence checker is verified with the Matita system. A unified framework for verified decision procedures for regular expression equivalence is presented in [13]. It is shown how three published decision procedures based on derivatives and two based on marked regular expressions (including the works presented in [3, 6, 12] ) can be obtained as instances of this framework. Proofs are obtained with Isabelle/HOL and an empirical comparison of performance of the considered decision procedures is presented. Marked regular expressions are also used in [5] to develop a matching algorithm verified with Coq which operates in linear time relative to the sizes of the input string and a regular expression. Other works are concerned with variants of matching algorithms: The computation of POSIX values, which provide information about which parts of an input string are matched by which part of a regular expression, is developed in [18] and correctness is proved with Isabelle/HOL. A matching algorithm for extended regular expression based on locations and Brzozowski derivatives is presented in [28] and verified with Lean. Based on Brzozowski’s matching algorithm, a lexical analyzer with runtime proportional to the square of the string length is developed in [7] and correctness is proved with Coq. The analyzer is optimized so that linear runtime is obtained and enhanced with additional features in [8]. A generator for lexical analyzers is presented in [14] and verified with Coq. Non-deterministic finite automatons (nfa) are synthesized for regular expressions in [9] and equivalence of matching with acceptance by the corresponding nfa is proved in Agda. Based on Brzozowski derivatives, a parser for regular expressions computing parse trees is developed in [16] and correctness is proved with Agda. 7 Conclusion When concerned with automated reasoning, the number of required user interactions for the proofs in a case study gives an impression about a system’s automation degree. \({{\checkmark }\hspace{-0.20cm} \texttt {eriFun} \hspace{-0.19cm}}\) provides three kinds of user support, viz. (1) formulation of a termination function for a procedure for which automated termination analysis fails, (2) formulation of an auxiliary lemma which is needed for a proof, and (3) application of an HPL-proof rule at some leaf of a proof tree when the system is unable to complete a proof automatically. Table 3 displays the effort for obtaining the proofs in three case studies of the paper, viz. for the correctness of Yi’s matching algorithm and of Brzozowski’s matcher with Antimirov derivatives and with Brzozowski derivatives respectively. The bottom row in Table 3 gives the statistics for the proof of Theorem 25. Column Proc. in Table 3 counts the number of user defined procedures with the number of user provided termination functions in parentheses, Lem. is the number of proven lemmas (with the number of those requiring user invoked HPL-proof rule applications in parentheses), User counts the total number of user invoked HPL-proof rule applications and System those which are automatically invoked by the system’s heuristics. The numbers in parentheses refer to the induction rule and demonstrate the success of the system’s heuristic when choosing Induction. Column % gives the automation degree, i.e. the ratio between System and Rules, Steps lists the total number of first-order proof steps performed by the Symbolic Evaluator and Sec displays the needed computer time in seconds.Footnote 4 The statistics also count the numbers for the program elements which had been imported from our Arithmetic- and List-library. As the system’s termination analysis failed for procedures \({\dag }\) and !, termination functions (coinciding with the argumentation given in [27]) have to be provided. The system then generates 9 termination hypotheses for \({\dag }\) and 24 termination hypotheses for ! and proves each of them automatically after 4 lemmas about the measure functions have been provided and proved. The remaining procedures terminate by structural recursion or lexicographic combinations thereof, so that the system trivially succeeds in the generation of the termination hypotheses and the computation of their proofs. While an automation degree of \(95\%\) and higher can be achieved in mathematically simple domains, e.g. when sorting lists (see Table 2 in [22]) or upon verification of tautology checkers [19], values of \(85\%\) and below usually are encountered for case studies in Number Theory, see [19, 26] for examples. This is because quite often elaborate ideas for developing a proof are needed in this difficult domain which are beyond the ability of the system’s heuristics guiding the proof search. This effect shows up also here to some extend: The completeness proof for procedure \({\dag }\) necessitated 20 user interventions, whereas soundness of \({\dag }\) and ! and completeness of ! only required 5, 5 and 4 user hints respectively. The reason is that one has to come up with the idea of splitting a non-empty word w into subwords \(u\ne \varepsilon \) and v, which is not suggested by the definitions. It also results in more complex proof obligations, so that the needed reasoning is not supported by the system’s heuristics. Once correctness of Yi’s matching algorithm ! is verified, the proofs for both Brzozowski matching procedures and procedure !! are easily obtained as they follow the same line of reasoning. As a consequence, this case study necessitated some work in the analysis of the proof obligations on which the system got stuck to come up with additional notions and fresh lemmas needed to complete a proof.Footnote 5 The system’s Disprover [1] often helped not to waste time with trying to prove a faulty conjecture, where the computed counter-examples provided useful information how to debug a lemma draft. Data Availability The proof files related to the paper are to be found under https://www.verifun.de. Code availability Notes Short for “A Verifier for Functional Programs”. Only tautologies hold (and can be proved) for calls of incompletely defined (and terminating) procedures with arguments not in the procedures’ domain, as e.g. \(\forall K\):\(\textit{list}[\Sigma ^{*} ],w\):\(\Sigma ^{*}\) \(U(w,{\o },K)=U(w,\)ø, K) and \(\forall L,K\):\(\textit{list}[\Sigma ^{*}],w\):\(\Sigma ^{*}\) U(w, ø\(,K)=V(w,L,{\o })\vee U(w,\)ø\(,K)\ne V(w,L,{\o })\). See [23] for the formal semantics of incomplete definitions. Observe that \(w\notin K\wedge w\in ~\)£\((r^{*},n)\otimes K\) implies £\((r^{*},n)\backslash \hspace{-0.08cm}\backslash \varepsilon \ne \) ø (and \(w\ne \varepsilon \) in turn) as otherwise \(w=\varepsilon \circ v\) with \(v\in K\), hence \(w=v\) contradicting \(w\notin K\). Time refers to running \(\checkmark \)eriFun 3.5 under Windows 7 Enterprise with an INTEL Core i5-2520M 2.50 GHz CPU using Java 1.8.0_311. The proofs in [27] did not help that much because they lack sufficient detail. However, proof steps causing work upon formal reasoning quite often are hidden in the gaps of a manual proof as usually one focuses on the essential ideas in a paper and omits proof steps regarded as “obvious”. References Aderhold, M., Walther, C., Szallies, D., Schlosser, A.: A Fast Disprover for eriFun. In W. Ahrendt, P. Baumgartner, and H. de Nivelle, editors, Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06), pages 59–69, Seattle, WA, (2006). https://verifun.de/documents Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996). https://doi.org/10.1016/0304-3975(95)00182-4 Asperti, A.: A compact proof of decidability for regular expression equivalence. In L. Beringer and A. P. Felty, editors, 3rd Intern. Conf. on Interactive Theorem Proving ITP, volume 7406 of Lect. Notes in Comp. Sc., pages 283–298, Princeton, USA, 2012. Springer. https://doi.org/10.1007/978-3-642-32347-8_19 Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964). https://doi.org/10.1145/321239.321249 Chattopadhyay, A., Li, A.W., Mamouras, K.: Verified and efficient matching of regular expressions with lookaround. In K. Stark, A. Timany, S. Blazy, and N. Tabareau, editors, Proc. 14th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs, CPP, pages 198–213, Denver, USA, (2025). ACM. https://doi.org/10.1145/3703595.3705884 Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In J. Jouannaud and Z. Shao, editors, 1st Intern. Conf. on Certified Programs and Proofs CPP, volume 7086 of Lect. Notes in Comp. Sc., pages 119–134, Kenting, Taiwan, (2011). Springer. https://doi.org/10.1007/978-3-642-25379-9_11 Egolf, D., Lasser, S., Fisher, K.: Verbatim: A verified lexer generator. In IEEE Security and Privacy Workshops, pages 92–100, San Francisco, USA, (2021). IEEE. https://doi.org/10.1109/SPW53761.2021.00022 Egolf, D., Lasser, S., Fisher, K.: Verbatim++: verified, optimized, and semantically rich lexing with derivatives. In A. Popescu and S. Zdancewic, editors, 11th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs, pages 27–39, Philadelphia, USA, (2022). ACM. https://doi.org/10.1145/3497775.3503694 Firsov, D., Uustalu, T.: Certified parsing of regular languages. In G. Gonthier and M. Norrish, editors, Proc. 3rd Intern. Conf. on Certified Programs and Proofs CPP, volume 8307 of LNCS, pages 98–113, Melbourne, Australia, (2013). Springer. https://doi.org/10.1007/978-3-319-03545-1_7 Harper, R.: Proof-Directed Debugging. J. Funct. Program. 9(4), 463–469 (1999). https://doi.org/10.1017/S0956796899003378 Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, 2nd edn. Languages and Computation. Pearson Addison-Wesley, Boston, MA (2001) Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Autom. Reason. 49(1), 95–106 (2012). https://doi.org/10.1007/S10817-011-9223-4 Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. In G. Klein and R. Gamboa, editors, Proc. 5th Intern. Conf. on Interactive Theorem Proving ITP, volume 8558 of LNAI, pages 450–466, Vienna, Austria, (2014). Springer. https://doi.org/10.1007/978-3-319-08970-6_29 Ouedraogo, W., Scherer, G., Straßburger, L.: Coqlex: Generating formally verified lexers. Art Sci. Eng. Program. 8(1), (2024) https://doi.org/10.22152/programming-journal.org/2024/8/3 Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173–190 (2009). https://doi.org/10.1017/S0956796808007090 Ribeiro, R.G., Bois, A.R.D.: Certified bit-coded regular expression parsing. In F. Mascarenhas, editor, Proc. 21st Brazilian Symp. on Programming Languages, SBLP, pages 4:1–4:8, Fortaleza, Brazil, (2017). ACM. https://doi.org/10.1145/3125374.3125381 Thompson, K.: Programming techniques: Regular expression search algorithm. C. ACM 11(6), 419–422 (1968). https://doi.org/10.1145/363347.363387 Urban, C.: POSIX lexing with derivatives of regular expressions. J. Autom. Reason. 67(3), 24 (2023). https://doi.org/10.1007/S10817-023-09667-1 VeriFun. https://www.verifun.de Walther, C.: On Proving the Termination of Algorithms by Machine. Artif. Intell. 71(1), 101–157 (1994). https://doi.org/10.1016/0004-3702(94)90063-9 Walther, C.: Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base. ACM Trans. on Math. Softw. 45(1), 9.1-9.7 (2019). https://doi.org/10.1145/3301317 Walther, C.: A Largely Automated Verification of GHC’s Natural Mergesort. In G. Ernst et al., editor, Go Where the Bugs Are, volume 15765 of Lect. Notes in Comp. Sc., pages 83–103. Springer, (2025). https://doi.org/10.1007/978-3-031-92196-4_5 Walther, C.: Reasoning About Incompletely Defined Programs. J. Autom. Reasoning 69(3), 1–48 (2025). https://doi.org/10.1007/s10817-025-09722-z Walther, C., Schweitzer, S.: Verification in the Classroom. J. Autom. Reasoning 32(1), 35–73 (2004). https://doi.org/10.1023/B:JARS.0000021872.64036.41 Walther, C., Schweitzer, S.: Automated Termination Analysis for Incompletely Defined Programs. In F. Baader and A. Voronkov, editors, Proc. of the 11th Inter. Conf. on Logic for Progr., Artif. Intell. and Reasoning (LPAR-11), volume 3452 of Lect. Notes in Artif. Intell., pages 332–346, Montevideo, Uruguay, (2005). Springer. https://doi.org/10.1007/978-3-540-32275-7_22 Walther, C., Wasser, N.: Fermat, Euler, Wilson - Three Case Studies in Number Theory. J. Autom. Reasoning 59(2), 267–286 (2017). https://doi.org/10.1007/s10817-016-9387-z Yi, K.: Educational Pearl: ‘Proof-Directed Debugging’ revisited for a First-Order Version. J. Funct. Program. 16(6), 663–670 (2006). https://doi.org/10.1017/S0956796806006149 Zhuchko, E., Veanes, M., Ebner, G.: Lean formalization of extended regular expression matching with lookarounds. In A. Timany, D. Traytel, B. Pientka, and S. Blazy, editors, Proc. 13th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs, pages 118–131, London, UK, (2024). ACM. https://doi.org/10.1145/3636501.3636959 Acknowledgements Thanks to both reviewers for several comments and suggestions which helped to improve the paper. Funding Open Access funding enabled and organized by Projekt DEAL. None Author information Authors and Affiliations Contributions CW wrote the manuscript text and prepared all figures. Corresponding author Ethics declarations Materials availability Competing interests The authors declare no competing interests. Additional information Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Rights and permissions Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. About this article Cite this article Walther, C. Formally Verified Matching of Regular Expressions. J Autom Reasoning 70, 18 (2026). https://doi.org/10.1007/s10817-026-09761-0 Received: Accepted: Published: Version of record: DOI: https://doi.org/10.1007/s10817-026-09761-0