Generating Structurally Complex Tests from Declarative Constraints

Speaker: Dr Sarfraz Khurshid

Time: 12:30pm-1:30pm, February 23rd, 2007

Location: Nueces 201 Conference Room

Abstract:

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. 

Biography

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.