The 2014 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 seventh time.
The Award-Winning Contribution
Concurrency is omnipresent in computer systems, at all levels, from concurrent software running over multi-core platforms, to distributed applications running over large-scale networks. The automated verification of such systems is a challenging problem, due to the highly complex interactions between their components. Standard verification algorithms based on systematic state-space exploration face the well-known state-explosion problem when applied to such systems: the size of the state space of concurrent systems grows exponentially in the number of their components.
A major approach for tackling this problem and developing scalable algorithms for automated verification of concurrent systems comes from so-called partial-order reduction (POR) techniques, which leverage the fact that there often are a huge number of computations that lead to the same observable states (i.e., states that are relevant for checking the property under consideration)
While the POR idea seems natural and simple in principle, the difficulty is in designing efficient search algorithms that determine on-the-fly, i.e., during the state-space exploration of the system, which branches to prune and which ones to explore, while ensuring (1) that redundant explorations are avoided, and (2) that the state-space exploration is still complete, i.e., no computation equivalence class (modulo reordering of independent actions) is missed. In the period of 1990-1994, Godefroid, Peled, Valmari, and Wolper investigated this problem and defined algorithms for solving it (see bibliography below), based on the notions of stubborn, sleep and ample sets, respectively. These algorithms constitute the basis of the POR approach to model checking, which has been subsequently developed further, extended to various classes of systems, and integrated into several verification methods and tools. These tools are now widely used and applicable both in academia and industry. Indeed, several robust and influential verification tools rely on POR, and this approach has been applied to many different contexts and continues to have impact to this day. Among the tools where POR techniques are used, one can mention: SPIN, Verisoft, FLAVERS, ISP, JPF, CHESS, and many other model-checking and systematic testing tools.
In summary, POR is one of the major contributions to the field of automated verification in the last two decades. Its development contributed in a crucial way to make model checking successful and practically applicable to concurrent systems. This success is due to the seminal work that Godefroid, Peled, Valmari, and Wolper did in the first half of the 1990's. With this award, the community recognizes the historical importance and the deep impact of their contribution.
1. P. Godefroid: Using Partial Orders to Improve Automatic Verification Methods. CAV 1990: 176-185
2. P. Godefroid, P. Wolper: A Partial Approach to Model Checking. Inf. Comput. 110(2): 305-326 (1994) -- preliminary version at LICS 1991, 406-415
3. P. Godefroid, P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2): 149-1164 (1993) -- preliminary version at CAV 1991, 332-342
4. D. Peled: All from One, One for All: on Model Checking Using Representatives. CAV 1993, 409-423
5. D. Peled: Combining Partial Order Reductions with On-the-fly Model-Checking. CAV 1994, 377-390
6. A. Valmari: A Stubborn Attack on State Explosion. Formal Methods in System Design 1(4): 297-322 (1992) -- preliminary version at CAV 1990, 156-165
7. A. Valmari: On-the-Fly Verification with Stubborn Sets. CAV 1993, 397-408
The CAV (Computer-Aided Verification)
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-sixth CAV conference was held in Vienna, Austria, from July 18 to July 22, 2014, as part of the Vienna Summer of Logic.