The 2011 CAV (Computer-Aided Verification)
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-
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.
The CAV (Computer Aided Verification)
This year's twenty-third CAV conference was held in Snowbird, Utah from July 14 to July 20, 2011.