Link: http://rers-challenge.org/2019/index.php?page=results

Franco Mazzanti (FMT Lab, ISTI) and Frédéric Lang (CONVECS, Grenoble, France) recently won all gold medals for the "Parallel CTL" and "Parallel LTL" tracks of the RERS 2019 challenge.

The RERS (Rigorous Examination of Reactive Systems) challenge is an international software competition held every year since 2011. RERS 2019 is the 9th edition of the challenge and it took place within ETAPS, the primary European forum for software science, as part of the TOOLympics series of software competitions organized to celebrate the 25th anniversary of the prestigious conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).

RERS 2019 featured several tracks covering sequential, parallel, and industrial problems. Each track provided a wealth of problems of increasing complexity, the most involved of which are expected to be beyond any individual state-of-the-art method or tool. The goal of the "Parallel CTL" track was to verify 180 properties expressed in the branching-time temporal logic CTL. These properties had to be evaluated on various complex systems, having up to 70 concurrent processes and 234 synchronization actions. Similarly, the goal of the "Parallel LTL" track was to verify, on the same complex systems, 180 properties expressed in the linear-time temporal logic LTL. Participants were given a period of only three weeks, starting from the publication of the RERS problems on the RERS web site, to compute and submit their answers.

To attack such difficult problems, Lang and Mazzanti, who had never met before, decided to join forces, and together they managed to evaluate all the 360 CTL and LTL properties correctly. To this aim, they designed new verification algorithms and reused the compositional verification techniques implemented in the CADP toolbox developed by CONVECS, together with additional software tools, such as KandISTI developed by Mazzanti at FMT, to cross-check some of the results provided by CADP. While the RERS challenge allows the participants to use all possible computing facilities, including supercomputers, the clever use of compositional verification techniques by Lang and Mazzanti enabled all problems to be solved in about 10 hours on a standard laptop.