The reults of the 2016 edition of the Model Checking Contest are out:

Since 2011, The Model Checking Contest is a yearly scientific event dedicated to the assessment of formal verification tools for concurrent systems.

As shown in the chart, ITS-Tools (http://ddd.lip6.fr), developed at LIP6, has been ranked first in the category State Space construction and also reaches the podium in several other cases.


The objective of the Model Checking Contest is to compare the efficiency of techniques according to characteristics of models. To do so, the Model Checking Contest compares tools on several classes of models with scaling capabilities (e.g. values that set up the «size» of its associated state space). Through the feedback on tools efficiency according to the selected benchmarks, we aim at identifying the techniques that can tackle a given type of problem (e.g. state space generation, deadlock detection, reachability analysis, causal analysis).

The results of the 2016 edition of the Model Checking Contest