CAV award 2017
Parosh Abdulla, Alain Finkel, Bengt Johnsson, and Philippe Schnoebelen receive the CAV Award 2017 for the development of general mathematical structures leading to general decidability results for the verification of infinite-state transition systems.
Influential Work on Well-Quasi Orders
Starting in the early 1990s, research focused on the automatic verification of infinite-state systems. Many of the results were obtained with highly nontrivial algorithms, and at that time, this new research area was lacking common methods and general principles.
This situation was addressed by the works of Parosh Abdulla, Alain Finkel, Bengt Johnsson, and Philippe Schnoebelen. In their seminal papers [1,2], they showed how the abstract notion of a well-quasi order can be used to identify a large class of infinite-state transition systems with important decidability properties.
Their work has had strong and lasting influence on the field: the general principles exposed in those papers were shown to be applicable to an impressively large number of formalisms. Equally important, well-quasi orders also have been at the heart of many practical contributions that target, among others, the automatic verification of multi-threaded programs and parametric systems.
Although infinite-state abstractions are canonical abstractions for concurrent systems composed of a fixed number of processes, infinite-state models, such as Petri nets and their extensions, are necessary for the analysis of systems where correctness should hold for any number of components, or for systems where dynamic creation of processes or threads of executions are allowed. While the automatic verification of such systems remains a challenging and active area of research, much progress has been made in the last few years and many practical contributions are grounded in the awardees’ works on well-quasi orders.
- Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay: General Decidability Theorems for Infinite-State Systems. LICS 1996: 313-321
- Alain Finkel, Philippe Schnoebelen:Well-structured Transition Systems Everywhere! Theor. Comput. Sci. 256(1-2): 63-92 (2001)
The CAV award is given annually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification. The award comes with a cash prize of US$10,000 shared equally among recipients.
For previous winners of the award, please see the main CAV award page .
- Tom Ball (Chair), Microsoft Research
- Kim G. Larsen, Aalborg University
- Natarajan Shankar, SRI International
- Pierre Wolper, Liege University