The QuickCheck manual states that they are randomly generating test cases [1]. This tool is build on top of Pex [2] which analyzes the byte code and uses the Z3

The QuickCheck manual states that they are randomly generating test cases [1]. This tool is build on top of Pex [2] which analyzes the byte code and uses the Z3 theorem prover [3] to systematically find inputs covering all code paths. This is really a impressive and powerful tool. You can have some fun with it at the Pex for fun site [4]. There is some secret code and you have to reimplement that code based on the test results generated by Pex comparing your implementation to the secret implementation. [1] http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html http://www.cse.chalmers.se/~rjmh/QuickCheck/manual.html [2] http://research.microsoft.com/en-us/projects/pex/ http://research.microsoft.com/en-us/projects/pex/ [3] http://research.microsoft.com/en-us/projects/z3m/ http://research.microsoft.com/en-us/projects/z3m/ [4] http://www.pexforfun.com/ http://www.pexforfun.com/