THE CADP NEWSLETTER - Nr. 12
April 10, 2019
This newsletter is available from the CADP Home page.
(CONVECS, Grenoble, France) and
(FMT, Pisa, Italy) recently won all
the gold medals for the "Parallel CTL" and "Parallel LTL" tracks of the
RERS 2019 challenge.
In 2019, the RERS (Rigorous Evaluation of Reactive Systems) challenge 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
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. The correct results were only known by the organizers
of the RERS challenge.
To attack such difficult problems, Lang and Mazzanti, who had never met
before, decided to join forces, and managed to evaluate all the 360 CTL
and LTL properties correctly. This was done by designing new verification
algorithms and by reusing the compositional verification techniques
implemented in the CADP toolbox
developed by CONVECS.
They also used additional software tools, such as
SPOT for converting LTL formulas
to Büchi automata, as well as
nuXmv to cross-check some of the
results provided by CADP.
Although the rules of the RERS challenge allow the participants to use
all possible computing facilities, including supercomputers, the
judicious use of compositional verification techniques by Lang and Mazzanti
enabled all problems to be solved in about 10 hours on a standard Dell laptop.
The two winners received awards of 625 euros offered by Springer
The picture to the right was taken during the reward ceremony organized in
Prague (Czech Republic) on April 6th, 2019. From left to right: Malte Mues,
Franco Mazzanti, Frédéric Lang, Bernhard Steffen, and Falk Howar.
The work of Frédéric Lang has been partly supported by the
is a software toolbox for the design
of asynchronous concurrent systems, such as communication protocols,
distributed systems, asynchronous circuits, multiprocessor architectures,
etc. Developed since the late 80s, CADP is one of the two oldest model
checkers that are still in use today. CADP is actively maintained and
finds many applications, both in academia and industry. In March 2019,
the 15,000th license of CADP was granted.
is a research project-team
common between Inria Grenoble
and the LIG
(Laboratoire d'Informatique de Grenoble, France), a joint research center
Univ. Grenoble Alpes
The activities of CONVECS focus on the formal modeling and verification
of asynchronous concurrent systems, which find applications in many
different domains. In particular, CONVECS develops and maintains the
(Formal Methods and Tools)
is a research team of ISTI-CNR
Italy). FMT is active in the fields of development and application of formal
notations, methods, and software support tools for the specification, design,
and verification of complex computer systems. These efforts are based mostly
on the foundational concepts and techniques of process algebras, temporal
logics, and model checking.
(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
features several tracks covering sequential, parallel, and industrial
problems. Each track provides 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 "Parallel CTL" track was created in
2018 and the "Parallel LTL" track in 2019.
SECURIOT-2 is a collaborative project funded by the French government's
FUI (Fonds Unique Interministériel
) and supported by four
competitiveness clusters (Minalogic, SCS, Systematic, and DERBI).
The goal of SECURIOT-2 is to develop a secure microcontroller that will
bring to the IoT environment a high level of security, similar to the one
of the secure transactions industry (banking cards and ePassports),
in conformity with the requirements of Common Criteria certification.
Started in September 2017 for three years and led by TIEMPO Secure,
SECURIOT-2 builds upon the expertise of its partners. The main
contributions of CONVECS in this project are the formal modeling and
verification using CADP of the secure microcontroller developed in
Back to the CADP Home Page