RegMatch

An executable regular expression (regexp) matcher as defined in the paper Proof-directed debugging revisited, proved correct in the Coq proof assistant.

Requirements

Definitions and proofs:

• Coq 8.9 or later
• Mathematical Components 1.7.0 or later (ssreflect)
• RegLang

Executable matcher:

• OCaml 4.02.3 (or later)
• menhir
• OCamlbuild
• ocamlfind

Building

One easy way to install the dependencies (ssreflect, RegLang, and menhir) is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install menhir coq-mathcomp-ssreflect coq-reglang

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.