2012 CAV (Computer Aided Verification) 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 2012 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 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;
The CAV (Computer-Aided Verification)