This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques. The MCC is part of a thriving group of scientific events dedicated to provide a fair evaluation of formal analysis tools, with the goal to push forward the state of the art and provide insights into the evolution of the involved technologies and approaches. We give details on the organization of the competition and on the ways we manage models and formulas. We also take a look at the evolution of the results over the 2018—2023 period, using the wide variety of data we collect each year, and report on the impact the MCC had on the competing tools.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023

  • Nicolas Amat,
  • Elvio Amparore,
  • Bernard Berthomieu,
  • Pierre Bouvier,
  • Silvano Dal Zilio,
  • Francis Hulin-Hubard,
  • Peter G. Jensen,
  • Loig Jezequel,
  • Fabrice Kordon,
  • Shuo Li,
  • Emmanuel Paviot-Adet,
  • Laure Petrucci,
  • Jiří Srba,
  • Yann Thierry-Mieg,
  • Karsten Wolf

摘要

This paper takes you behind the scenes of the Model Checking Contest (MCC), an annual competition focusing on the behavioral analysis of asynchronous systems using state-space exploration and model checking techniques. The MCC is part of a thriving group of scientific events dedicated to provide a fair evaluation of formal analysis tools, with the goal to push forward the state of the art and provide insights into the evolution of the involved technologies and approaches. We give details on the organization of the competition and on the ways we manage models and formulas. We also take a look at the evolution of the results over the 2018—2023 period, using the wide variety of data we collect each year, and report on the impact the MCC had on the competing tools.