Symposium on Software, Science and Society

Department of Computer Science and Engineering
_______________________

HOME
Friday, December 5, 2003

AGENDA

SPEAKERS

TESTIMONIALS / COMMENTS

DICK'S ACCOUNT of CSE's early history

DIRECTIONS to World Forestry Center, 4033 S.W. Canyon Road, Portland, Oregon, including MAX information. Event is in Cheatham Hall.

REGISTER ONLINE
______________________

















SPEAKER PROFILE
HALF-DAY TECHNICAL SYMPOSIUM ON
SOFTWARE, SCIENCE & SOCIETY

Friday, December 5, 2003
Cheatham Hall • World Forestry Center • Portland, Oregon

THOMAS BALL
Microsoft Corporation
  BIOGRAPHY:

Thomas Ball is a Senior Researcher and head of the Testing, Verification and Measurement Research group in Microsoft Research. Ball joined Microsoft Research in the summer of 1999, with the goal of applying program analysis and programming language technology to hard problems in software correctness and reliability. Ball and Sriram Rajamani originated the SLAM project which pioneered fundamental advances in software model checking and its application to checking temporal safety properties of system software. The SLAM analysis engine forms the core of the Static Driver Verifier technology which is being taken to product by the Windows Driver Quality team in BaseOS.

Previous to Microsoft Research, Ball was a researcher at Bell Laboratories in AT&T (1993-1996) and then at Lucent Technologies (1996-1999), in the Software Production Research Department. Ball graduated with a Ph.D. in Computer Science from the University of Wisconsin-Madison in 1993.

ABSTRACT:

The SLAM project has pioneered fundamental advances in software mode checking and its application to checking temporal safety properties of system software The goal of the SLAM analysis engine is to statically check whether or not a C program obeys ``API contracts" that specify what it means to be a good client of an API. The engine has two unique aspects: it does not require a programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as ``counterexample-driven refinement''. The SLAM engine forms the core of the Static Driver Verifier technology which is being developed by the Windows development organization.