Results of the 2020 Model Checking Contest

Our tool, TINA, won a gold medal in the “state space” category of the Model-Checking Contest 2020, an international competition of model-checking tools for the verification of concurrent systems. This is the second year in a row that TINA came first in the “state space” category.

You can find more about how we managed to obtain this result by looking at the following publications:

References

#

• Presentation of the 9th Edition of the Model Checking Contest

  Verification Petri Contest Tina

  Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal Zilio, Francesco Gallà, Lom Messan Hillah, Francis Hulin-Hubard, Peter Gjøl Jensen, Loïg Jezequel, Fabrice Kordon, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Andrew Miner, Emmanuel Paviot-Adet, Jiří Srba, Yann Thierry-Mieg, Tom van Dijk, Karsten Wolf In TACAS 2019 — Tools and Algorithms for the Construction and Analysis of Systems, apr 2019.

• Petri Net Reductions for Counting Markings

  Verification Petri Tina Reductions

  Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio In SPIN 2018 — International Symposium on Model Checking Software, jun 2018.

• Counting Petri net markings from reduction equations

  Verification Reductions Petri Tina

  Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio International Journal on Software Tools for Technology Transfer (STTT) :1—19, apr 2019.