Papers related to the model checking contest

• L. Hillah and F. Kordon. Petri Nets Repository: a tool to benchmark and debug Petri Net tools. In 38th International Conference on Petri Nets and Other Models of Concurrency (ICATPN), volume 10258 of Lecture Notes in Computer Science, pages 125-135, Zaragoza, Spain, June 2017. Springer

  @inproceedings{hk2017,
    author = {{L. M.} Hillah and F. Kordon},
    title = {{Petri Nets Repository: a tool to benchmark and debug Petri Net tools}},
    booktitle = {{38th International Conference on Petri Nets and Other Models of Concurrency (Petri Nets)}},
    year = {2017},
    pages = {125-135},
    address = {Zaragoza, Spain},
    volume={10258},
    month={June},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science}}

• F. Kordon, H. Garavel, L. Hillah, E. Paviot-Adet, L. Jezequel, C. Rodriguez, and F. Hulin-Hubard. MCC'2015 - The Fifth Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), XI:262-273, 2016

  @Article{kghpajrhh2016,
    author = {Fabrice Kordon and Hubert Garavel and Lom{-}Messan Hillah and
      Emmanuel Paviot{-}Adet and Lo{\"{\i}}g Jezequel and C{\'{e}}sar
      Rodr{\'{\i}}guez and Francis Hulin{-}Hubard},
    title = {{MCC'2015 - The Fifth Model Checking Contest}},
    journal = {{Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)}},
    volume = {XI},
    year = {2016},
    pages = {262--273},
    publisher = {Springer Verlag}}

• F. Kordon and F. Hulin-Hubard. BenchKit, a Tool for Massive Concurrent Benchmarking. In 14th International Conference on Application of Concurrency to System Design - ACSD, pages 159-165, Tunis, Tunisia, June 2014. IEEE Computer Society

  @inproceedings{khh2014,
    author = {F. Kordon and F. Hulin-Hubard},
    title = {{BenchKit, a Tool for Massive Concurrent Benchmarking}},
    booktitle = {{14$^{th}$ International Conference on Application of Concurrency to System Design -- ACSD}},
    address = {Tunis, Tunisia},
    year = {2014},
    month = {June},
    pages = {159-165},
    publisher = {IEEE Computer Society}}

• F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, K. Lampka, N. Lohmann, E. Paviot- Adet, Y. Thierry-Mieg, and H. Wimmel. Report on the Model Checking Contest at Petri Nets 2011. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), VI:169-196, march 2012

  @Article{klbcellpatmw2012,
    author = {F. Kordon and A. Linard and D. Buchs and M. Colange and S. Evangelista and K. Lampka and
      N. Lohmann and E. Paviot-Adet and Y. Thierry-Mieg and H. Wimmel},
    title = {{Report on the Model Checking Contest at Petri Nets 2011}},
    journal = {{Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)}},
    volume = {VI},
    month = {march},
    year = {2012},
    pages = {169-196},
    publisher = {Springer Verlag}}

Results of the past years

• 2017: F. Kordon, H. Garavel, L. M. Hillah, F. Hulin-Hubard, B. Berthomieu, G. Ciardo, M. Colange, S. Dal Zilio, E. Amparore, M. Beccuti, T. Liebke, J. Meijer, A. Miner, C. Rohr, J. Srba, Y. Thierry-Mieg, J. van de Pol, and K. Wolf. Complete Results for the 2017 Edition of the Model Checking Contest

  @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}}
  

• 2016: F. Kordon, H. Garavel, L. M. Hillah, F. Hulin-Hubard, G. Chiardo, A. Hamez, L. Jezequel, A. Miner, J. Meijer, E. Paviot-Adet, D. Racordon, C. Rodriguez, C. Rohr, J. Srba, Y. Thierry- Mieg, G. Tr.inh, and K. Wolf. Complete Results for the 2016 Edition of the Model Checking Contest.

  @misc{mcc:2016,
    Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and
      G. Chiardo and A. Hamez and L. Jezequel and A. Miner and J. Meijer and E. Paviot-Adet
      and D. Racordon and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and
      G. Tr{\d i}nh and K. Wolf},
    Howpublished = {{http://mcc.lip6.fr/2016/results.php}},
    Lastchecked = {2016},
    Urldate = {2016},
    Month = {June},
    Title = {{Complete Results for the 2016 Edition of the Model Checking Contest}},
    Year = {2016}}

• 2015: F. Kordon, H. Garavel, L. M. Hillah, F. Hulin-Hubard, A. Linard, M. Beccuti, A. Hamez, E. Lopez-Bobeda, L. Jezequel, J. Meijer, E. Paviot-Adet, C. Rodriguez, C. Rohr, J. Srba, Y. Thierry-Mieg, and K. Wolf. Complete Results for the 2015 Edition of the Model Checking Contest.

  @misc{mcc:2015,
    Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and A. Linard and
      M. Beccuti and A. Hamez and E. Lopez-Bobeda and L. Jezequel and J. Meijer and E. Paviot-Adet
      and C. Rodriguez and C. Rohr and J. Srba and Y. Thierry-Mieg and K. Wolf},
    Howpublished = {{http://mcc.lip6.fr/2015/results.php}},
    Lastchecked = {2015},
    Title = {{Complete Results for the 2015 Edition of the Model Checking Contest}},
    Urldate = {2015},
    Year = {2015}}

• 2014: F. Kordon, H. Garavel, L.-M. Hillah, F. Hulin-Hubard, A. Linard, M. Beccuti, S. Evangelista, A. Hamez, N. Lohmann, E. Lopez, E. Paviot-Adet, C. Rodriguez, C. Rohr, and J. Srba. HTML results from the Model Checking Contest @ Petri Net (2014 edition).

  @misc{mcc:2014,
    Author = {F. Kordon and H. Garavel and L-M. Hillah and F. Hulin-Hubard and A. Linard and
      M. Beccuti and S. Evangelista and A. Hamez and N. Lohmann and E. Lopez and
      E. Paviot-Adet and C. Rodriguez and C. Rohr and J. Srba},
    Howpublished = {{http://mcc.lip6.fr/2014}},
    Lastchecked = {2014},
    Title = {{HTML results from the Model Checking Contest @ Petri Net (2014 edition)}},
    Urldate = {2014},
    year = {2014}}

• 2013: F. Kordon, A. Linard, M. Beccuti, D. Buchs, L. Fronc, L. Hillah, F. Hulin-Hubard, F. Legond-Aubry, N. Lohmann, A. Marechal, E. Paviot-Adet, F. Pommereau, C. Rodriguez, C. Rohr, Thierry-Mieg, H. Wimmel, and K. Wolf. Model checking contest @ petri nets, report on the 2013 edition. CoRR, abs/1309.2485, 2013.

  @article{mcc:2013,
    author = {Fabrice Kordon and Alban Linard and Marco Beccuti and Didier Buchs and
      Lukasz Fronc and Lom{-}Messan Hillah and Francis Hulin{-}Hubard and
      Fabrice Legond{-}Aubry and Niels Lohmann and Alexis Marechal and
      Emmanuel Paviot{-}Adet and Franck Pommereau and C{\'{e}}sar Rodr{\'{\i}}guez and
      Christian Rohr and Thierry{-}Mieg and Harro Wimmel and Karsten Wolf},
    title = {Model Checking Contest @ Petri Nets, Report on the 2013 edition},
    journal = {CoRR},
    volume = {abs/1309.2485},
    year = {2013},
    url = {http://arxiv.org/abs/1309.2485},
    archivePrefix = {arXiv},
    eprint = {1309.2485}}

• 2012: F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, L. Fronc, L. Hillah, N. Lohmann, E. Paviot- Adet, F. Pommereau, C. Rohr, Y. Thierry-Mieg, H. Wimmel, and K. Wolf. Raw report on the model checking contest at petri nets 2012. CoRR, abs/1209.2382, 2012.

  @article{mcc:2012,
    author = {Fabrice Kordon and Alban Linard and Didier Buchs and Maximilien Colange and
      Evangelista and Lukasz Fronc and Lom-Messan Hillah and Niels Lohmann
      and Emmanuel Paviot{-}Adet and Franck Pommereau and Christian Rohr and
      Yann Thierry{-}Mieg and Harro Wimmel and Karsten Wolf},
    title = {Raw Report on the Model Checking Contest at Petri Nets 2012},
    journal = {CoRR},
    volume = {abs/1209.2382},
    year = {2012},
    url = {http://arxiv.org/abs/1209.2382},
    archivePrefix = {arXiv},
    eprint = {1209.2382}}

Some Scientific Papers Mentioning the Model Checking Contest

1. Petri Net Synthesis with Union/Find (2018)
2. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets (2018)
3. Petri Net Reductions for Counting Markings (2018)
4. Assessing SMT and CLP approaches for workflow nets verification (2018)
5. Generation of Minimum Tree-Like Witnesses for Existential CTL (2018)
6. Towards Reliable Benchmarks of Timed Automata (2018)
7. Decision diagrams for Petri nets: a comparison of variable ordering algorithms (2018)
8. Petri Net Model Checking with LoLA 2 (2018)
9. Self-adaptive Model Checking, the Next Step (2018)
10. A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning (2018)
11. A Distributed Fixed-Point Algorithm for Extended Dependency Graphs (2018)
12. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (2018)
13. Generation of Minimum Tree-Like Witnesses for Existential CTL (2018)
14. Property-Preserving Generation of Tailored Benchmark Petri Nets (2017)
15. Explicit state model checking with generalized Büchi and Rabin automata (2017)
16. Stubborn Versus Structural Reductions for Petri Nets (2017)
17. Property-Preserving Parallel Decomposition (2017)
18. Industrial applications of the PetriDotNet modelling and analysis tool (2017)
19. A hybrid model checking approach to analysing rule conformance applied to HIPAA privacy rules (2017)
20. Petri Nets Repository: A Tool to Benchmark and Debug Petri Net Tools (2017)
21. The physics of software tools: SWOT analysis and vision (2017)
22. Extended Dependency Graphs and Efficient Distributed Fixed-Point Computation (2017)
23. Reduction of Workflow Nets for Generalised Soundness Verification (2017)
24. Faster Simulation of (Coloured) Petri Nets Using Parallel Computing (2017)
25. Decision Diagrams for Petri Nets: which Variable Ordering? (2017)
26. TAPAAL and Reachability Analysis of P/T Nets (2016)
27. A toolchain on model checking SPIN via Kalman Decomposition for control system software (2016)
28. A Term Rewriting Approach to Analyze High Level Petri Nets (2016)
29. Multi-core SCC-Based LTL Model Checking (2016)
30. A Symbolic Model Checker for Petri Nets: pnmc (2016)
31. Running LoLA 2.0 in a Model Checking Competition (2016)
32. MARCIE's Secrets of Efficient Model Checking (2016)
33. MCC'2015 - The Fifth Model Checking Contest (2016)
34. Component-wise Incremental LTL Model Checking (2016)
35. A Method of Sample Models of Program Construction in Terms of Petri Nets (2015)
36. Génération de règles de coordination à partir de réseaux de Petri colorés (2015)
37. Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets (2015)
38. Building a Symbolic Model Checker from Formal Language Description (2015)
39. Saturation-Based Incremental LTL Model Checking with Inductive Proofs (2015)
40. New Search Strategies for the Petri Net CEGAR Approach (2015)
41. Vers l'intégration de paramètres temporels statiques et dynamiques dans les techniques de vérification par ordre partiel (2014)
42. Bounded Model Checking High Level Petri Nets in PIPE+Verifier (2014)
43. PeCAn: Compositional Verification of Petri Nets Made Easy (2014)
44. Formal Modeling and Analysis Techniques for High Level Petri Nets (2014)
45. Teaching formal methods: Experience at UPMC and UP13 with CosyVerif (2014)
46. BenchKit, a Tool for Massive Concurrent Benchmarking (2014)
47. Petri Nets Research at BTU in Cottbus, Germany (2014)
48. Read, Write and Copy Dependencies for Symbolic Model Checking (2014)
49. Compilation de réseaux de Petri : modèles haut niveau et symétries de processus (2014)
50. Formal verification problems in a big data world: towards a mighty synergy (2014)
51. Advanced Saturation-based Model Checking (2014)
52. Distributed CTL Model Checking in the Cloud (2013)
53. Compilation de réseaux de Petri (2013)
54. Verifiable Design of a Satellite-based Train Control System with Petri Nets (2014)
55. Unifying the syntax and semantics of modular extensions of Petri nets (2013)
56. Modeling and Analyzing Wireless Sensor Networks with VeriSensor : An Integrated Workflow (2013)
57. Building Petri nets tools around Neco compiler (2013)
58. LTL Model Checking with Neco (2013)
59. MaRDiGraS : Simplified Building of Reachability Graphs on Large Clusters (2013)
60. CosyVerif: An Open Source Extensible Verification Environment (2013)
61. A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems (2013)
62. Unifying the syntax and semantics of modular extensions of Petri nets (2013)
63. Half a century after Carl Adam Petri's Ph.D. thesis: A perspective on the field (2013)
64. Verification based on unfoldings of Petri nets with read arcs (2013)
65. High-level Petri net model checking : the symbolic way (2012)
66. Stubborn Sets for Simple Linear Time Properties (2012)
67. High-Level Petri Net Model Checking with AlPiNA (2011)
68. Crocodile : A Symbolic/Symbolic Tool for the Analysis of Symmetric Nets with Bag (2011)