Automated Test Generation Using a Constraint Solver

For programs that manipulate complex structures, generating a good test suite is difficult and laborious. This talk presents an approach for generating a suite completely automatically. The user needs to provide only an invariant or precondition characterizing the acceptable inputs, and a bound on input size. A tool then generates a collection of appropriate test cases, using a constraint solver as the underlying engine.

The talk explains the details of this approach and describes experience applying it to various problems, ranging from library code to stand-alone applications. Experiments on checking some methods from the Java Collection Framework indicate that it is feasible to systematically generate a high quality test suite. The tool also uncovered previously unknown errors in several applications: an intentional naming scheme developed for the MIT Oxygen project, a constraint solver for first-order relational logic, and a fault-tree analysis system developed for NASA.
Sarfraz Khurshid is an Assistant Professor of Electrical and Computer Engineering at the University of Texas at Austin. He received his PhD in Computer Science at MIT in 2004. He received a BSc in Mathematics and Computer Science from Imperial College (London), and read Part III of the Mathematical Tripos at Trinity College (Cambridge). His current research focuses on software testing, specification languages, code conformance, model checking, and applications of heuristics in program analysis.