2011 CAV Award for Groundbreaking Work in Software Verification

Sept. 26, 2011 - PRLog -- 2011 CAV Award Announcement

The 2011 CAV (Computer-Aided Verification) Award was presented on July 17, 2011 at the 23rd annual CAV conference in Snowbird, Utah to Thomas Ball and Sriram Rajamani of Microsoft Research. The annual award, which recognizes a specific fundamental contribution or a series of outstanding contributions to the CAV field includes a $10,000 award. The award was presented with the citation:  “for their contributions to software model checking, specifically the development of the SLAM/SDV software model checker, which successfully demonstrated computer-aided verification techniques on real programs.”

The CAV conference is the premier international event for reporting research on Computer Aided Verification, a sub-discipline of Computer Science that is concerned with ensuring that software and hardware systems operate correctly and reliably.  The CAV award was established in 2008 by the conference steering committee and was given this year for the third time.

The Award-Winning Contribution

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 worthy recipients of the
2011 CAV Award.

CAV Conference

The CAV (Computer Aided Verification) conference is an annual international conference dedicated to the advancement of the theory and practice of computer aided formal analysis methods for hardware and software systems.  The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation.  The CAV conference was founded in 1989 by Edmund M. Clarke, Robert P. Kurshan, Amir Pnueli, and Joseph Sifakis.  The first CAV conference was hosted in 1989 in Grenoble, France, and since then it has been held in multiple sites in North America, Europe, and the Middle East.

This year's twenty-third CAV conference was held in Snowbird, Utah from July 14 to July 20, 2011.