A computer system provides a test program and one or more unit tests, such
as a traditional unit test and or a parameterized unit test. The system
also includes a constraint solver, a theorem prover, an implementation
under test, a symbolic executor, a generalizor, and generated test cases.
The generalizor receives a traditional unit tests as input, and modifies
the traditional unit test into a parameterized unit test. The
modification includes replacing plural concrete values in the traditional
unit test with symbols, and exporting the symbols into a signature of the
parameterized unit test. A symbolic executor identifies constraints while
symbolically executing the created parameterized unit test of the
implementation under test. A constraint solver and or theorem prover
generates a set of test cases by solving for values that satisfy the
series of constraints. The test program executes the automatically
generated test cases.