The 2011 CAV Award

The annual CAV Award has been established for a specific fundamental contribution or a series of outstanding contributions to the field of Computer Aided Verification. The award of $10,000 is granted to an individual or a group of individuals chosen by the Award Committee from a list of nominations. The committee may choose to make no award. The CAV Award is presented in an award ceremony at CAV and a citation is published in Formal Methods in System Design.

The 2011 CAV Award is given to Thomas Ball and Sriram Rajamani for their contributions to software model checking, specifically the development of the SLAM/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs.

In the late 1990s, a key challenge for Microsoft was operating system reliability, due, in a large measure, to the low quality of device drivers. By some estimates, drivers caused 70-85% of kernel failures. Ball and Rajamani focused their attention on ensuring that device drivers were well-behaved. In order to do this, they invented a formalism (SLIC) for expressing correct behavior, built an engine (c2bp) for abstracting C programs to Boolean programs, and wrote a model checker (Bebop) for Boolean programs. The resulting technology could be applied to programs with tens of thousands of lines of code. They also added a counterexample-driven abstraction refinement step (newton) and characterized the theoretical power of the method. The project eventually led to the Static Driver Verifier tool that is used by third-party driver developers and is distributed with the Windows Driver Kit.

This research showed how theorem proving, model checking, and static analysis technology can be applied to real programs of realistic size written in real programming languages. Critics could no longer argue that computer-aided verification was limited to hardware or to toy programs. The SLAM project represents a turning point in the acceptance and adoption of software verification technology in industrial applications. The project had a large impact within Microsoft, triggering major investments in verification research, leading to new languages and verification tools that are widely adopted within the company. The SLAM project also significantly influenced research outside of Microsoft. It is fair to say that SLAM was instrumental in restarting research by the formal methods and programming languages communities in program verification, a subject that had been moribund for quite some time.

It is very rare to see a research idea go from conception to industrial impact in such a short duration. The direct contributions of this work, both in developing a new approach to verifying temporal safety properties of software and turning this result into an industrially important software tool, combined with its influence and impact in the research community make Thomas Ball and Sriram Rajamani appropriate candidates for the 2011 CAV Award.

Thomas Ball is Principal Researcher and Research Manager at Microsoft Research. 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. Tom's interests range from program analysis, model checking, testing and automated theorem proving to the problems of defining and measuring software quality.

Sriram Rajamani is Assistant Managing Director at Microsoft Research India, where he also leads the Rigorous Software Engineering group. Sriram's research interests are in programming languages, programming tools, verification tools, formal methods, and the interplay between logical and statistical reasoning. Sriram got his Ph.D. in Computer Science from UC Berkeley.