I just learnt that Radu Mateescu, Hubert Garavel, Frédéric Lang and Wendelin Serwe from the Construction of Verified Concurrent Systems (Convecs) project team at INRIA Grenoble – Rhône-Alpes Centre have been recently awarded the Inria Innovation Prize – Académie des sciences – Dassault Systèmes. Their work contributes to the development of the CADP toolbox for modelling and verifying parallel and distributed systems. The aim of that project is to automatically detect design flaws in highly complex systems.
Readers of this blog will be as delighted as I am by this news. CADP is one of the tools from the concurrency community that has the longest history, dating back to its early releases in 1989. It has been used to good effect in a variety of applications, is still under continuous development and makes excellent use in practice of classic tools from concurrency theory. By way of example, let me mention the recent successes by the Convecs team in dealing with difficult challenges posed by Bernhard Steffen and his team on the evaluation of CTL and LTL formulae on large products of automata. (See, for instance, the news items here and here.) Traditional model checkers fail on those challenges because the state space of the product automata is too large for them. However, a wise use of bisimulations and congruence results allows CADP to solve many of those challenges. Interested readers might also wish to peruse the slides at
Congratulations to the whole CADP team and to the concurrency community for this award!
No comments:
Post a Comment