The 2008 CAV (Computer Aided Verification) award is given to Rajeev Alur from the University of Pennsylvania and David L. Dill from Stanford University for fundamental contributions to the theory of real-time systems verification.
The CAV award is an annual award given for a specific fundamental contribution or a series of outstanding contributions to the field of Computer Aided Verification. Computer Aided Verification is the subdiscipline of Computer Science that is concerned with ensuring that software and hardware systems operate correctly and reliably.
The CAV award has been established by the steering committee of the annual CAV (Computer Aided Verification) conference. The CAV conference is the premier international event for reporting Computer Aided Verification research.
The CAV award carries a $10,000 prize and was presented at this year's CAV conference on July 10, 2008, in Princeton, New Jersey. This is the first year that the CAV award is given.
The 2008 CAV award is given for the seminal 1990 article on "Automata for modeling real-time systems" by Alur and Dill. This article laid the theoretical foundation for the computer aided verification of real-time systems, which are computer systems that are expected to finish their computations by specific deadlines. With the increasing ubiquity of embedded computers, which control everything from aircraft to medical devices, there is an urgent need for a rigorous methodology that can ensure that such systems operate without failures.
During the late 1980's there were several attempts to extend the theory of computer aided verification to real-time systems. Alur and Dill's work put this research direction on a firm foundational footing. In particular, the formalism of Timed Automata introduced by Alur and Dill in their 1990 paper has become the standard model for the verification of real-time systems. The 1990 paper of Alur and Dill is among the most cited papers in Computer Aided Verification.
Dr. Alur is Zisman Family Professor in the Department of Computer and Information Science at University of Pennsylvania. He obtained his bachelor's degree in computer science from the Indian Institute of Technology at Kanpur in 1987, and PhD in computer science from Stanford University in 1991. Before joining the University of Pennsylvania in 1997, he was with the Computing Science Research Center at Bell Laboratories. Dr. Alur's research spans formal modeling and analysis of reactive systems, hybrid systems, model checking, software verification, and design automation for embedded software. His awards include the President of India's Gold Medal for academic excellence, a CAREER award of the US National Science Foundation, and an Alfred P. Sloan Faculty Fellowship. He is a Fellow of the ACM, a Fellow of the IEEE, and recently served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems).
Dr. Dill is a Professor of Computer Science and, by courtesy, Electrical Engineering at Stanford University, where he has been on the faculty since 1987. He has an SB in Electrical Engineering and Computer Science from the Massachusetts Institute of Technology (1979) and a PhD from Carnegie-Mellon University (1987). Dr. Dill has research interests in a variety of areas, including computational systems biology, the theory and application of formal verification techniques to system designs, and voting technology. He has also done research in asynchronous circuit verification and synthesis, and in verification methods for hard real-time systems. He was one of the founders and the Chief Scientist of 0-In Design Automation (later acquired by Mentor Graphics), and the founder of the non-profit organizations Verified Voting Foundation and VerifiedVoting.org. His awards include the ACM's Distinguished Dissertation award for his PhD thesis, a Presidential Young Investigator award from the National Science Foundation, a Young Investigator award from the Office of Naval Research, and the Electronic Frontier Foundation's Pioneer Award (for work in electronic voting). He is a Fellow of the IEEE and ACM.
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.
This year's anniversary twentieth CAV conference was held in Princeton, New Jersey, from July 7 to 14, 2008. The current members of the steering committee of the CAV conference are Edmund M. Clarke from Carnegie-Mellon University, Michael J.C. Gordon from the University of Cambridge (United Kingdom), Robert P. Kurshan from Cadence Design Systems, and Amir Pnueli from New York University.