2014 CAV (Computer-Aided Verification Conference) Award Announcement

By: CAV Conference
VIENNA - July 20, 2014 - PRLog -- 2014 CAV Award Announcement

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

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-sixth CAV conference was held in Vienna, Austria, from July 18 to July 22, 2014, as part of the Vienna Summer of Logic.
End
Source:CAV Conference
Email:***@cs.ox.ac.uk Email Verified
Tags:Cav Award
Industry:Education, Research
Location:Vienna - Vienna - Austria
Account Email Address Verified     Account Phone Number Verified     Disclaimer     Report Abuse
Page Updated Last on: Jul 20, 2014



Like PRLog?
9K2K1K
Click to Share