A design verification system generates a small set of test cases, from a finite state machine model of the application under test. The finite state machine is reduced by creating efficient samples of the inputs to the application under test which are prepared by combinatorial input parameter selection. The test cases are generated by finite state machine traversal of the reduced state machine, and tests interacting combinations of input parameters in an efficient way. The technique is integrated into a test generator based on a finite state machine. Using an extended language, partial rulesets are employed to instruct the test generator to automatically employ combinatorial input parameter selection during test generation. Another technique for test case generation is disclosed, which uses combinatorial selection algorithms to guarantee coverage of the system under test from the aspect of interaction between stimuli at different stages or transitions in the test case.