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.

1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay: General Decidability Theorems for Infinite-State Systems. LICS 1996: 313-321

2. Alain Finkel, Philippe Schnoebelen:Well-structured Transition Systems Everywhere! Theor. Comput. Sci. 256(1-2): 63-92 (2001)

CAV Award