Towards verified regular expression matchers in hardware

Abstract Regular expression matching is used in a wide variety of applicationsranging from compilers to computational biology. We are interested inthis task because of their usefulness in runtime verification, whichis used to ensure the correctness of reactive systems. Runtimeverification involves the design and use of a monitor which observesthe behaviour of a running system and flags deviations from a formalspecification describing its intended behaviour. The effectiveness ofruntime verification depends on the correctness of the monitor. Hence,the confidence in overall system correctness can be enhanced if themonitor is proven to be correct. In this work, we provide a mechanism that accepts a generalized formof regular expressions within the theorem prover Coq and produces thehardware implementation for a corresponding matcher. The resultantmatchers are reasonably small and can be used in practicalapplications like monitoring liveness properties. Our experimentalresults show that our designs have reasonably low resource utilizationwith the growth in their size limited to linear bounds. Hence, designsare useful for practical use cases. Info -Title: Towards verified regular expression matchers in hardware -Type: MS Thesis