An executable regular expression (regexp) matcher as defined in the paper Proof-directed debugging revisited, proved correct in the Coq proof assistant.
This project is used as a small motivating example of proof engineering in the paper QED at Large: A Survey of Engineering of Formally Verified Software. The key certified functions mentioned in the paper are acc in regmatch.v and acc' in regmatch_reglang.v.
Definitions and proofs:
Coq 8.9 or laterMathematical Components 1.9.0 or later(ssreflect)Ott 0.30 or later(and its Coq library)RegLangEquations
Executable matcher:
OCaml 4.05(or later)menhirOCamlbuildocamlfind
Make sure the ott program is in the PATH, and Ott's Coq auxiliary library has been installed under Coq's user-contrib directory. Also make sure the RegLang and ssreflect Coq libraries have been installed.
One easy way to install ssreflect, RegLang, Equations, menhir, and Ott and its Coq library is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install menhir ott coq-mathcomp-ssreflect coq-reglang coq-ott coq-equations
Then, run make. This will compile the Coq syntax and relation definitions along with the proofs and functions, and extract OCaml code.
To build the executable matcher program, run make matcher.