For programs that manipulate complex structures, generating a good test suite is difficult and laborious. We have developed a novel 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. This talk explains the details of the 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. The talk also presents an overview of the methodologies the Software Verification and Testing Group at the UT is developing for increasing software reliability.
Sarfraz Khurshid is an Assistant Professor in the Electrical and Computer Engineering department at the University of Texas at Austin, where he leads the Software Verification and Testing Group. He completed his PhD in Computer Science at the Massachusetts Institute of Technology 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, data structure repair, and applications of heuristics in program analysis.