2014 CAV Award Announcement
The 2014 CAV Award was presented on July 19, 2014, at the 26th annual CAV conference in Vienna, to Patrice Godefroid, Doron Peled, Antti Valmari, and Pierre Wolper. The annual award, which recognizes a specific fundamental contribution or a series of outstanding contributions to computer-aided verification includes a $10,000 award. The award was presented with the citation: “for the development of partial-order-reduction algorithms for efficient state-space exploration of concurrent systems.”
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), but differ only in the order in which some parallel actions are interleaved. These actions are actually independent of one another (in the sense that they are not conflicting, so partially ordered), thus, their total ordering in a particular execution is not relevant. Therefore, the idea is to consider such computations as equivalent, so that only one representative of each equivalence class needs to be considered during the state-space exploration. The notion of independence was first formulated in 1977 by Antoni Mazurkiewicz, and has been studied since then in the context of concurrency semantics by a number of authors. Nevertheless, it was not until the first half of 1990s that these ideas have been applied in algorithmic verification.
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.
Bibliography:
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-164 (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
2014 CAV Award Committee
- Marta Kwiatkowska , Trinity College Oxford
- Ahmed Bouajjani , Univ. Paris Diderot (Paris 7)
- Tom Ball , Microsoft Research
- Moshe Vardi, Rice University