White-Box Testing: We discuss here a framework that combines symbolic execution and model-checking techniques for automated test case generation in the context of Java programs. The framework is typically used for test input generation for white-box testing. The framework model checks program under test. Test case generation is guided by a testing coverage criterion, e.g., branch coverage. The model checker explores systematically the paths of the program under test and records the paths that satisfy the coverage criterion. Symbolic execution, that is performed throughout model checking, computes a symbolization that is, a set of constraints, of all the inputs that execute those paths. The actual testing requires solving the input constraints in order to produce concrete test inputs that can be executed.