Presentation of the 9th Edition of the Model Checking Contest

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

doi:10.1007/978-3-030-17502-3_4

Presentation of the 9th Edition of the Model Checking Contest

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

^*Corresponding author for this work

Formal Methods and Tools

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

20 Citations (Scopus)

42 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS
Subtitle of host publication	TOOLympics, Held as Part of ETAPS 2019, Proceedings
Editors	Fabrice Kordon, Marieke Huisman, Bernhard Steffen, Dirk Beyer
Publisher	Springer
Pages	50-68
Number of pages	19
ISBN (Print)	9783030175016
DOIs	https://doi.org/10.1007/978-3-030-17502-3_4
Publication status	Published - 4 Apr 2019
Event	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 - Charles University, Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019 Conference number: 25

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11429 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019
Abbreviated title	TACAS 2019
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 11/04/19
Other	held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

Keywords

Competition
CTL formulas
LTL formulas
Model checking
Reachability formulas
State space

Access to Document

10.1007/978-3-030-17502-3_4Licence: CC BY

Amparore-2019-Presentation-of-the-th-edition-of-tFinal published version, 824 KBLicence: CC BY

Cite this

Amparore, E., Berthomieu, B., Ciardo, G., Dal Zilio, S., Gallà, F., Hillah, L. M., Hulin-Hubard, F., Jensen, P. G., Jezequel, L., Kordon, F., Le Botlan, D., Liebke, T., Meijer, J., Miner, A., Paviot-Adet, E., Srba, J., Thierry-Mieg, Y., van Dijk, T., & Wolf, K. (2019). Presentation of the 9th Edition of the Model Checking Contest. In F. Kordon, M. Huisman, B. Steffen, & D. Beyer (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings (pp. 50-68). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11429 LNCS). Springer. https://doi.org/10.1007/978-3-030-17502-3_4

Amparore, Elvio ; Berthomieu, Bernard ; Ciardo, Gianfranco et al. / Presentation of the 9th Edition of the Model Checking Contest. Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings. editor / Fabrice Kordon ; Marieke Huisman ; Bernhard Steffen ; Dirk Beyer. Springer, 2019. pp. 50-68 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1f938362edd44696806e3a1a7b06e5fe,

title = "Presentation of the 9th Edition of the Model Checking Contest",

abstract = "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{\^A}to 3600{\^A}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.",

keywords = "Competition, CTL formulas, LTL formulas, Model checking, Reachability formulas, State space",

author = "Elvio Amparore and Bernard Berthomieu and Gianfranco Ciardo and {Dal Zilio}, Silvano and Francesco Gall{\`a} and Hillah, {Lom Messan} and Francis Hulin-Hubard and Jensen, {Peter Gj{\o}l} and Lo{\"i}g Jezequel and Fabrice Kordon and {Le Botlan}, Didier and Torsten Liebke and Jeroen Meijer and Andrew Miner and Emmanuel Paviot-Adet and Ji{\v r}{\'i} Srba and Yann Thierry-Mieg and {van Dijk}, Tom and Karsten Wolf",

year = "2019",

month = apr,

day = "4",

doi = "10.1007/978-3-030-17502-3_4",

language = "English",

isbn = "9783030175016",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "50--68",

editor = "Fabrice Kordon and Marieke Huisman and Bernhard Steffen and Dirk Beyer",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS",

note = "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , TACAS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

}

Amparore, E, Berthomieu, B, Ciardo, G, Dal Zilio, S, Gallà, F, Hillah, LM, Hulin-Hubard, F, Jensen, PG, Jezequel, L, Kordon, F, Le Botlan, D, Liebke, T, Meijer, J, Miner, A, Paviot-Adet, E, Srba, J, Thierry-Mieg, Y, van Dijk, T & Wolf, K 2019, Presentation of the 9th Edition of the Model Checking Contest. in F Kordon, M Huisman, B Steffen & D Beyer (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11429 LNCS, Springer, pp. 50-68, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17502-3_4

Presentation of the 9th Edition of the Model Checking Contest. / Amparore, Elvio; Berthomieu, Bernard; Ciardo, Gianfranco et al.
Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings. ed. / Fabrice Kordon; Marieke Huisman; Bernhard Steffen; Dirk Beyer. Springer, 2019. p. 50-68 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11429 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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, Jiří

AU - Thierry-Mieg, Yann

AU - van Dijk, Tom

AU - Wolf, Karsten

N1 - Conference code: 25

PY - 2019/4/4

Y1 - 2019/4/4

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 - Conference contribution

AN - SCOPUS:85064938998

SN - 9783030175016

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 50

EP - 68

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS

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

Y2 - 6 April 2019 through 11 April 2019

ER -

Amparore E, Berthomieu B, Ciardo G, Dal Zilio S, Gallà F, Hillah LM et al. Presentation of the 9th Edition of the Model Checking Contest. In Kordon F, Huisman M, Steffen B, Beyer D, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings. Springer. 2019. p. 50-68. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-17502-3_4

Presentation of the 9th Edition of the Model Checking Contest

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this