Proving correctness of regular expression matchers with constrained repetition

It is known that an often used implementation method for regular expressions that uses a combination of counters and nondeterministic finite automatons is incorrect for certain regular expressions. Determining which expressions can be correctly implemented with this method has proven nontrivial and has previously been done without proof. Presented is the first automatic method to prove the correctness of the implementation method for specific expressions and to detect which expressions should be implemented differently. The use (in previous work) of this implementation method in network intrusion detection systems without proof of correctness for every regular expression constitutes a security risk to the network it is supposed to protect. Presented is a solution for this issue.