2011 CAV Award for Groundbreaking Work in Software Verification

The 2011 Computer-Aided Verification Award was presented in July 2011 to Thomas Ball and Sriram Rajamani of Microsoft Research.

Houston (I-Newswire) September 28, 2011 - 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.

About Rice University


Contact Information

Rice University
Moshe Vardi
6100 Main Street
Rice University
Phone : 713-348-4834


Software   award   verification  

Published in:

Computer > Software

Published On:

September 28, 2011

Print Release:

Print Release

If you have questions regarding information in this press release contact the company listed above. I-Newswire.com is a press release service and not the author of this press release.The information that is on or available through this site is for informational purposes only and speaks only as of the particular date or dates of that information. As some companies and PR Agencies submit their press releases once per week,month or quarter, make sure to check the official company website for accurate release dates as our site displays the I-Newswire.com press release distribution date only.We do not guarantee the accuracy or completeness of information on or available through this site, and we are not responsible for or omissions in that information or for actions taken in reliance on that information.

Related Releases

Election Aspiring App Developers in India
With General elections in full swing, all areas of society are bustling with political activities. App development is not an exception to this. Politics challenge is one of the most interesting game launched on similar lines.

Perform Effective Code Reviews with Code Review Bundle
Devart offers the new Code Review Bundle, which allows developers to conduct the code review process on all development stages.

1000 Free Copies of Beefed-up MacX DVD Ripper Pro for 2014 Easter Day Are Available at MacXDVD
With the Easter Day upon us, MacXDVD launches the 2014 Easter giveaway event to celebrate the festival. During the Easter promotion, 1000 copies of the updated MacX DVD Ripper Pro are totally free of charge before April 25th, 2014.

PC Service Manager More Powerful
PC Service Manager, a complete online management suite for PC service centers announces that the newest release of its application includes powerful new benefits.

Significant Benefits of Playing Online Cricket Games
It is one the best online cricket games to have with the online friends.