Results for the MCC@Petri Net 2017
- the Complete Results for the 2017 Edition of the Model Checking Contest,
- the slides presented in Zaragoza.
If you want to cite the 2017 MCC report, please proceed as follows (bibtex entry):
@misc{mcc:2017, Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and B. Berthomieu and G. Ciardo and M. Colange and S. {Dal Zilio} and E. Amparore and M. Beccuti and T. Liebke and J. Meijer and A. Miner and C. Rohr and J. Srba and Y. Thierry-Mieg and J. van de Pol and K. Wolf}, Howpublished = {{http://mcc.lip6.fr/2017/results.php}}, Lastchecked = {2017}, Month = {June}, Title = {{Complete Results for the 2017 Edition of the Model Checking Contest}}, Urldate = {2017}, Year = {2017}}
This should look like to this (useful for those who prefer word-like word processors ;-):
Objectives
The Model Checking Contest is a yearly scientific event dedicated to the assessment of formal verification tools for concurrent systems.
The Model Checking Contest has two different parts: the Call for Models, which gathers Petri net models proposed by the scientific community, and the Call for Tools, which benchmarks verification tools developed within the scientific community.
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 Model Checking Contest is composed of two calls: a call for models and a call for tools.
After six editions in 2011, 2012, 2013, 2014, 2015, and 2016, this is the seventh one that will take place at PETRI NETS 2017 in Zaragoza.
Results of the Previous Editions
Below is a quick access to the results of the past editions of the Model Checking Contest:
- MCC'2016 @ Torún: slides - HTML report
- MCC'2015 @ Brussels: slides - HTML report
- MCC'2014 @ Tunis: slides - HTML report
- MCC'2013 @ MIlano: slides - HTML report - PDF report (CoRR)
- MCC'2012 @ Hamburg: slides - PDF report (CoRR)
- MCC'2011 @ Newcastle: slides - report (ToPnoC link)
Important dates
- Dec. 15, 2016: publication of the present Call for Models
- Dec. 19, 2016: publication of the present Call for Tools
- Jan. 15, 2017: publication of the Tool Submission Kit, which will be made available from http://mcc.lip6.fr/archives/ToolSubmissionKit.tar.gz
- Jan. 15, 2017: publication of the updated 2017 contest rules at http://mcc.lip6.fr/rules.php
- Feb. 1st, 2017: deadline for tool pre-registration If you plan to submit a tool to the contest, please fill in the pre-registration form (you may retire if you finally decide not to do so)
- Feb. 15, 2017: deadline for model submission
- Apr. 15, 2017: individual notification of model acceptance/rejection
- Apr. 15, 2017: deadline for tool submission
- Apr. 30, 2017: early feedback to tool submitters, following the preliminary qualification runs, which are performed using a few small instances of the "known" models
- June 1, 2017: on-line publication of the selected MCC'2017 models
- June 27, 2017: official announcement of MCC'2017 results during the Petri Net conference (Zaragoza, Spain)
Scientific Papers Mentioning the Model Checking Contest
- Industrial applications of the PetriDotNet modelling and analysis tool (2017)
- A hybrid model checking approach to analysing rule conformance applied to HIPAA privacy rules (2017)
- Petri Nets Repository: A Tool to Benchmark and Debug Petri Net Tools (2017)
- The physics of software tools: SWOT analysis and vision (2017)
- Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation (2017)
- Reduction of Workflow Nets for Generalised Soundness Verification (2017)
- Faster Simulation of (Coloured) Petri Nets Using Parallel Computing (2017)
- Decision Diagrams for Petri Nets: which Variable Ordering? (2017)
- TAPAAL and Reachability Analysis of P/T Nets (2016)
- A toolchain on model checking SPIN via Kalman Decomposition for control system software (2016)
- A Term Rewriting Approach to Analyze High Level Petri Nets (2016)
- Multi-core SCC-Based LTL Model Checking (2016)
- A Symbolic Model Checker for Petri Nets: pnmc (2016)
- Running LoLA 2.0 in a Model Checking Competition (2016)
- MARCIE's Secrets of Efficient Model Checking (2016)
- MCC'2015 - The Fifth Model Checking Contest (2016)
- Component-wise Incremental LTL Model Checking (2016)
- Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets (2015)
- Building a Symbolic Model Checker from Formal Language Description (2015)
- Saturation-Based Incremental LTL Model Checking with Inductive Proofs (2015)
- New Search Strategies for the Petri Net CEGAR Approach (2015)
- Bounded Model Checking High Level Petri Nets in PIPE+Verifier (2014)
- PeCAn: Compositional Verification of Petri Nets Made Easy (2014)
- Formal Modeling and Analysis Techniques for High Level Petri Nets (2014)
- Teaching formal methods: Experience at UPMC and UP13 with CosyVerif (2014)
- BenchKit, a Tool for Massive Concurrent Benchmarking (2014)
- Petri Nets Research at BTU in Cottbus, Germany (2014)
- Read, Write and Copy Dependencies for Symbolic Model Checking (2014)
- Compilation de réseaux de Petri : modèles haut niveau et symétries de processus (2014)
- Formal verification problems in a big data world: towards a mighty synergy (2014)
- Advanced Saturation-based Model Checking (2014)
- Distributed CTL Model Checking in the Cloud (2013)
- Compilation de réseaux de Petri (2013)
- Verifiable Design of a Satellite-based Train Control System with Petri Nets (2014)
- Unifying the syntax and semantics of modular extensions of Petri nets (2013)
- Modeling and Analyzing Wireless Sensor Networks with VeriSensor : An Integrated Workflow (2013)
- Building Petri nets tools around Neco compiler (2013)
- LTL Model Checking with Neco (2013)
- MaRDiGraS : Simplified Building of Reachability Graphs on Large Clusters (2013)
- CosyVerif: An Open Source Extensible Verification Environment (2013)
- A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems (2013)
- Unifying the syntax and semantics of modular extensions of Petri nets (2013)
- Half a century after Carl Adam Petri’s Ph.D. thesis: A perspective on the field (2013)
- Verification based on unfoldings of Petri nets with read arcs (2013)
- High-level Petri net model checking : the symbolic way (2012)
- Stubborn Sets for Simple Linear Time Properties (2012)
- High-Level Petri Net Model Checking with AlPiNA (2011)
- Crocodile : A Symbolic/Symbolic Tool for the Analysis of Symmetric Nets with Bag (2011)