2012 CAV (Computer Aided Verification) Award Announcement

July 12, 2012 - PRLog -- 2012 CAV Award Announcement

The 2012 CAV (Computer-Aided Verification) Award was presented on July 11, 2012, at the 24th annual CAV conference in Berkeley, California, to Sam Owre, John Rushby, and Natarajan Shankar of SRI International. 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 developing PVS (Prototype Verification System) which, due to its early emphasis on integrated decision procedures and user friendliness, significantly accelerated the application of proof assistants to real-world verification problems."

The CAV conference is the premier international event for reporting research on Computer-Aided Verification, a sub-discipline of Computer Science which 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 fifth time.

The Award-Winning Contribution

The design of automatic theorem provers has been one of the great challenges in Computer Science since its beginnings, with the hope that computers - by searching through infinite but well-defined spaces of formal proofs - would be able to determine whether a mathematical hypothesis is a theorem and, ultimately, discover interesting new mathematics. In parallel to the difficult task of finding entire proofs automatically, much focus has been on the more limited goal of building interactive proof assistants, which are programs that support a user in constructing formal arguments and point out gaps in the reasoning. Several such systems were already successful in the early 1990s, when Sam Owre, John Rushby, and Natarajan Shankar of SRI International built PVS (Prototype Verification System) - a proof assistant that was specifically designed to be used in system verification.

In verification, proofs demonstrate the absence of errors in a software or hardware system. Such proofs tend to overwhelm humans not by their mathematical depth, but by the enormous number of steps, cases, side conditions, and the like, which need to be considered. For a correctness proof to be completed successfully, it is often more important for a computer to relieve the user of simple steps and manage the overall progress of the argument, rather than provide or check deep mathematical insights. At a time when much research in computer-aided verification focused on semantic approaches such as model checking, Owre, Rushby, and Shankar made proof assistants fashionable in verification by building PVS around the following key elements:

1. An expressive, user-friendly, and well-documented system specification language
2. Programmable tactics for automatically exploring promising proof directions
3. Decision procedures for common logical theories and their combination

Especially the third element - the pioneering conviction of the critical importance of decision procedures, which automatically take care of many small, but tedious steps in a proof - has proved prescient and led to an explosion of research in decision procedures over past 20 years. Today, almost no sizable verification project can succeed without decision procedures, and most employ the help of proof management tools in one form or another. PVS paved that way by orienting proof assistants toward greater speed and usability, at a time when most others focused dogmatically on soundness.

PVS has found avid user communities especially in the verification of safety-critical applications; real-time, distributed, and security protocols; requirements engineering and software tools - all areas where both are essential: (i) the ability, provided by expressive languages, to reason about infinite-state systems and (ii) the automation provided by efficient, integrated decision procedures.  With this award, the CAV community recognizes the historical importance of PVS and the associated paper "PVS: A Prototype Verification System" by Sam Owre, John Rushby, and Natarajan Shankar, which appeared at the Conference on Automated Deduction (CADE) in 1992.

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-fourth CAV conference was held in Berkeley, California, from July 7 to July 13, 2012.