TY - GEN
T1 - Presentation of the 9th Edition of the Model Checking Contest
AU - Amparore, Elvio
AU - Berthomieu, Bernard
AU - Ciardo, Gianfranco
AU - Dal Zilio, Silvano
AU - Gallà, Francesco
AU - Hillah, Lom Messan
AU - Hulin-Hubard, Francis
AU - Jensen, Peter Gjøl
AU - Jezequel, Loïg
AU - Kordon, Fabrice
AU - Le Botlan, Didier
AU - Liebke, Torsten
AU - Meijer, Jeroen
AU - Miner, Andrew
AU - Paviot-Adet, Emmanuel
AU - Srba, Jiri
AU - Thierry-Mieg, Yann
AU - van Dijk, Tom
AU - Wolf, Karsten
PY - 2019/1/1
Y1 - 2019/1/1
N2 - The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with upÂto 3600Âs and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.
AB - The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing benchmark gathered from the whole community and may participate in various examinations: state space generation, computation of global properties, computation of some upper bounds in the model, evaluation of reachability formulas, evaluation of CTL formulas, and evaluation of LTL formulas. For each examination and each model instance, participating tools are provided with upÂto 3600Âs and 16 gigabyte of memory. Then, tool answers are analyzed and confronted to the results produced by other competing tools to detect diverging answers (which are quite rare at this stage of the competition, and lead to penalties). For each examination, golden, silver, and bronze medals are attributed to the three best tools. CPU usage and memory consumption are reported, which is also valuable information for tool developers.
KW - Competition
KW - CTL formulas
KW - LTL formulas
KW - Model checking
KW - Reachability formulas
KW - State space
UR - http://www.scopus.com/inward/record.url?scp=85064938998&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-17502-3_4
DO - 10.1007/978-3-030-17502-3_4
M3 - Article in proceeding
AN - SCOPUS:85064938998
SN - 9783030175016
T3 - Lecture Notes in Computer Science
SP - 50
EP - 68
BT - International Conference on Tools and Algorithms for the Construction and Analysis of Systems
A2 - Kordon, Fabrice
A2 - Huisman, Marieke
A2 - Steffen, Bernhard
A2 - Beyer, Dirk
PB - Springer
T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
Y2 - 6 April 2019 through 11 April 2019
ER -