Formally Verified Matching of Regular Expressions
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 repo...