At Microsoft, we have been advancing the state-of-the-art in testing through the application of automated techniques such as model checking and symbolic execution. First, I'll show how to automatically find errors in multithreaded software by systematic exploration of thread schedules, using concepts from model checking. These ideas are realized in a tool called CHESS (http://research.microsoft.com/projects/chess ) that finds errors such as data-races, deadlocks, hangs, and data-corruption induced access violations, errors that are extremely hard to find with traditional testing methods. Second, I'll show how the processes of fuzz and unit testing can be improved via knowledge of program internals, using symbolic execution of program paths and automated theorem provers. Tools from Microsoft, such as SAGE and Pex (http://research.microsoft.com/pex/), incorporate these techniques and are in regular use at Microsoft.

Biography:

Thomas Ball is Principal Researcher at Microsoft Research where he manages the Software Reliability Research group (http://research.microsoft.com/srr/). Tom started graduate school 20 years ago in 1987 and graduated with a Ph.D. in 1993. Tom is fast becoming a veteran of industrial research labs, having worked from 1993-1999 at Bell Labs in AT&T and Lucent Technologies and since 1999 at Microsoft Research. He is one of the originators of the SLAM project, a software model checking engine for C that forms the basis of the Static Driver Verifier tool, made freely available by Microsoft for finding defects in device drivers. Tom's interests range from program analysis, model checking, testing and automated theorem proving to the problems of defining and measuring software quality. Tom’s website is http://research.microsoft.com/~tball/

Refreshments served in OLS 224 after seminar.