Title:  Program Analysis 2.0

Abstract:  Microsoft Research's efforts in program analysis began with detecting defects in C and C++ programs with tools such as ESP, PREfast, PREfix, and SLAM, all of which have been widely deployed internally. The PREfast and SLAM technologies also were incorporated into shipping Microsoft products (Visual Studio and the Driver Development Kit, respectively).

In the last few years, we have been working on program analysis tools for .NET, focusing on: (1) code contracts and verifying code against contracts; (2) automatic test generation; (3) checking for concurrency defects. These tools are based on advances in abstract interpretation over linear inequalities, symbolic execution of object-oriented programs, efficient and precise automatic theorem proving, and direct model checking of concurrent systems. All of the above tools are available for both academic and commercial use, in partnership with Visual Studio.

For more information about Microsoft Research in this area, visit their RiSE website

Bio:  Thomas Ball is Principal Researcher at Microsoft Research where he manages the Software Reliability Research group. Tom received a Ph.D. from the University of Wisconsin-Madison in 1993, was with Bell Labs from 1993-1999, and has been at Microsoft Research since 1999. 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. Tom's interests range from program analysis, model checking, testing and automated theorem proving to the problems of defining and measuring software quality.

Live Video Stream:  GoToMeeting
Phone Bridge:  916-356-2663, 8-356-2663, Bridge: 4, Passcode: 2782812