Practical example: how to formally verify "file name" implementation from a spec?
In general, the technique used is known as "fuzzing". Not all errors are equally likely. Let's consider two hypothetical errors:


System A incorrectly rejects a filename if it contains an | anywhere.
System A incorrectly rejects a filename if it contains a prime number of b characters.


Errors of the second type are much, much rarer, but this is not explained by Computer Science. It's a result from how humans construct software. Fuzzing tries to focus on typical human bugs. In this case, we can predict the following types of errors are more likely:


Very short paths and very long paths may have boundary errors.
Errors near the begin or end of the path are more common than errors at the end
Many characters can be organized into classes which are treated identically, such as lowercase characters. All characters in this class are treated equally, so whether a filename is valid does not depend on a substitution within the class.
Some characters are a priori known to be problematic and each should be treated as a class on its own. (Examples: &lt;&gt;/\&amp;:")
Duplicating characters is more likely to cause bugs the closer they're together.


Fuzzing aims to generate a smaller set of strings by omitting irrelevant variations. We obviously generate an initial set of testcases of all possible lengths (1-200). This checks rule 1. We then expand this set by varying a few characters near both ends. We might try varying the 150th character of the 170 character testcase, but we won't bother with all 254 variations. Nor will we add a variation in the 151th character.