Table of contents
- Papers related to the model checking contest
- Results of the past years
- Some Scientific Papers Mentioning the Model Checking Contest
Papers related to the model checking contest
-
F. Kordon, L. M. Hillah, F. Hulin-Hubard, L. Jezequel, and E. Paviot-Adet. Study
of the efficiency of model checking techniques using results of the mcc from 2015
to 2019. International Journal on Software Tools for Technology Transfer, 2021.
@article{khhjp2021,
author = {Kordon, Fabrice and Hillah, Lom Messan and Hulin-Hubard,
Francis and Jezequel, Lo{\"\i}g and Paviot-Adet, Emmanuel},
title = {Study of the efficiency of model checking techniques using
results of the MCC from 2015 To 2019},
journal = {International Journal on Software Tools for Technology Transfer},
doi = {10.1007/s10009-021-00615-1},
isbn = {1433-2787},
url = {https://doi.org/10.1007/s10009-021-00615-1},
year = {2021}}
-
E. G. Amparore, B. Berthomieu, G. Ciardo, S. Dal-Zilio, F. Gallà, L. Hillah,
F. Hulin-Hubard, P. G. Jensen, L. Jezequel, F. Kordon, D. L. Botlan, T. Liebke,
J. Meijer, A. S. Miner, E. Paviot-Adet, J. Srba, Y. Thierry-Mieg, T. van Dijk,
and K. Wolf. Presentation of the 9th edition of the model checking contest. In
Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of
TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April
6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer
Science, pages 50–68. Springer, 2019.
@inproceedings{abcdg2019,
author = {Elvio Gilberto Amparore and Bernard Berthomieu and Gianfranco Ciardo and
Silvano Dal{-}Zilio and Francesco Gall{\`{a}} and Lom{-}Messan Hillah and
Francis Hulin{-}Hubard and Peter Gj{\o}l Jensen and Lo{\"{\i}}g Jezequel and
Fabrice Kordon and Didier Le Botlan and Torsten Liebke and
Jeroen Meijer and Andrew S. Miner and Emmanuel Paviot{-}Adet and
Jir{\'{\i}} Srba and Yann Thierry{-}Mieg and Tom van Dijk and
Karsten Wolf},
title = {Presentation of the 9th Edition of the Model Checking Contest},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague,
Czech Republic, April 6-11, 2019, Proceedings, Part {III}},
series = {Lecture Notes in Computer Science},
volume = {11429},
publisher = {Springer},
pages = {50--68},
year = {2019}}
- F. Kordon, H.
Garavel, L. Hillah, E. Paviot-Adet, L. Jezequel, F. Hulin-Hubard, E. G.
Amparore, M. Beccuti, B. Berthomieu, H. Evrard, P. G. Jensen, D. L. Botlan, T.
Liebke, J. Meijer, J. Srba, Y. Thierry-Mieg, J. van de Pol, and K. Wolf.
MCC'2017 - the seventh model checking contest. Transactions on Petri Nets and
Other Models of Concurrency (ToPNoC), XIII:181-209, 2018.
@article{kghpjh2019,
author = {Fabrice Kordon and Hubert Garavel and Lom{-}Messan Hillah and
Emmanuel Paviot{-}Adet and Lo{\"{\i}}g Jezequel and Francis Hulin{-}Hubard and
Elvio Gilberto Amparore and Marco Beccuti and Bernard Berthomieu and
Hugues Evrard and Peter Gj{\o}l Jensen and
Didier Le Botlan and Torsten Liebke and Jeroen Meijer and
Jir{\'{\i}} Srba and Yann Thierry{-}Mieg and Jaco van de Pol and
Karsten Wolf},
title = {MCC'2017 - The Seventh Model Checking Contest},
journal = {Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)},
volume = {XIII},
pages = {181--209},
year = {2018},
publisher = {Springer Verlag}} -
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
- 2022: F. Kordon, P.
Bouvier, H. Garavel, F. Hulin-Hubard, N. Amat, E. Amparore, B. Berthomieu, D.
Donatelli, S. Dal Zilio, P. Jensen, L. Jezequel, C. He, S. Li, E. Paviot-Adet,
J. Srba, and Y. Thierry-Mieg. Complete Results for the 2022 Edition of the
Model Checking Contest. http://mcc.lip6.fr/2022/results.php, June 2022.
@misc{mcc:2022,
Author = {F. Kordon and P. Bouvier and H. Garavel and F. Hulin-Hubard and
N. Amat and E. Amparore and B. Berthomieu and D. Donatelli and
S. {Dal Zilio} and {P. G.} Jensen and L. Jezequel and C. He and S. Li and
E. Paviot-Adet and J. Srba and Y. Thierry-Mieg},
Howpublished = {{http://mcc.lip6.fr/2022/results.php}},
Lastchecked = 2022,
Month = {June},
Title = {{Complete Results for the 2022 Edition of the Model Checking Contest}},
Urldate = {2022},
Year = {2022}}
- 2021: F. Kordon, P.
Bouvier, H. Garavel, L. M. Hillah, F. Hulin-Hubard, N. Amat, E. Amparore, B.
Berthomieu, S. Biswal, D. Donatelli, F. Galla, S. Dal Zilio, P. Jensen, L.
Jezequel, C. He, D. Le Botlan, S. Li, E. Paviot-Adet, J. Srba, Y. Thierry-Mieg,
A. Walner, and K. Wolf. Complete Results for the 2021 Edition of the Model
Checking Contest. http://mcc.lip6.fr/2021/results.php, June 2021
@misc{mcc:2021,
Author = {F. Kordon and P. Bouvier and H. Garavel and L. M. Hillah and F. Hulin-Hubard and
N. Amat and E. Amparore and B. Berthomieu and S. Biswal and D. Donatelli and
F. Galla and and S. {Dal Zilio} and {P. G.} Jensen and L. Jezequel and C. He and
D. {Le Botlan} and S. Li and E. Paviot-Adet and J. Srba and Y. Thierry-Mieg and
A. Walner and K. Wolf},
Howpublished = {{http://mcc.lip6.fr/2021/results.php}},
Lastchecked = 2021,
Month = {June},
Title = {{Complete Results for the 2021 Edition of the Model Checking Contest}},
Urldate = {2021},
Year = {2021}} - 2020: F. Kordon, H.
Garavel, L. M. Hillah, F. Hulin-Hubard, E. Amparore, B. Berthomieu, S. Biswal,
D. Donatelli, F. Galla, G. Ciardo, S. Dal Zilio, P. Jensen, L. Jezequel, D. Le Botlan, S.
Li, A. Miner, E. Paviot-Adet, J. Srba, and Y. Thierry-Mieg. Complete Results for the 2020
Edition of the Model Checking Contest. June 2020
@misc{mcc:2020,
Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and
E. Amparore and B. Berthomieu and S. Biswal and D. Donatelli and
F. Galla and G. Ciardo and S. {Dal Zilio} and {P. G.} Jensen and , L. Jezequel and
D. {Le Botlan} and S. Li and A. Miner and E. Paviot-Adet and J. Srba and Y. Thierry-Mieg},
Howpublished = {{http://mcc.lip6.fr/2020/results.php}},
Lastchecked = 2020,
Month = {June},
Title = {{Complete Results for the 2020 Edition of the Model Checking Contest}},
Urldate = {2020},
Year = {2020}}
- 2019: F. Kordon, H.
Garavel, L. M. Hillah, F. Hulin-Hubard, E. Amparore, M. Beccuti, B. Berthomieu,
G. Ciardo, S. Dal Zilio, L. Jezequel, T. Liebke, S. Li, J. Meijer, A. Miner, E. Paviot-Adet, J. Srba, Y.
Thierry-Mieg, J. van de Pol, T. van Dirk, and K. Wolf. Complete Results for the
2019 Edition of the Model Checking Contest. April 2019.
@misc{mcc:2019, Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and
E. Amparore and M. Beccuti and B. Berthomieu and G. Ciardo and S. {Dal Zilio} and
L. Jezequel and T. Liebke and S. Li and J. Meijer and A. Miner and E. Paviot-Adet and
J. Srba and Y. Thierry-Mieg and J. van de Pol and T. van Dirk and K. Wolf},
Howpublished = {{http://mcc.lip6.fr/2019/results.php}},
Lastchecked = 2019,
Month = {April},
Title = {{Complete Results for the 2019 Edition of the Model Checking Contest}},
Urldate = {2019},
Year = {2019}} - 2018: F. Kordon and
H. Garavel and L. M. Hillah and F. Hulin-Hubard and E. Amparore and M. Beccuti
and B. Berthomieu and G. Ciardo and S. {Dal Zilio} and T. Liebke and A. Linard
and J. Meijer and A. Miner and J. Srba and Y. Thierry-Mieg and J. van de Pol
and K. Wolf. Complete Results for the 2018 Edition of the Model Checking
Contest
@misc{mcc:2018, Author = {F. Kordon and H. Garavel and L. M. Hillah and F. Hulin-Hubard and
E. Amparore and M. Beccuti and B. Berthomieu and G. Ciardo and S. {Dal Zilio} and
T. Liebke and A. Linard and J. Meijer and A. Miner and J. Srba and
JY. Thierry-Mieg and J. van de Pol and K. Wolf},
Howpublished = {{http://mcc.lip6.fr/2018/results.php}},
Lastchecked = {2018},
Month = {June},
Title = {{Complete Results for the 2018 Edition of the Model Checking Contest}},
Urldate = {2018},
Year = {2018}}
- 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
- Pinpointing Conflicts in Temporal Knowledge Bases via Model Checking (2023)
- Efficient Strategies to Compute Invariants, Bounds and Stable Places of Petri nets (2023)
- Implementing a CTL Model Checker with μ G, a Language for Programming Graph Neural Networks (2023)
- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition (2023)
- Anti-Patterns (Smells) in Temporal Specifications (2023)
- SMPT: A Testbed for Reachability Methods in Generalized Petri Nets (2023)
- Leveraging polyhedral reductions for solving Petri net reachability problems (2023)
- Introduction to the special issue for SPIN 2021 (2023)
- Leveraging polyhedral reductions for solving Petri net reachability problems (2022)
- A Decision Diagram Operation for Reachability (2022)
- Model-checking ecological state-transition graphs (2022)
- LTL Under Reductions with Weaker Conditions Than Stutter Invariance (2022)
- From Spot 2. to pot 2.10 : what's new?' (2022)
- Verifiable Biology (2022)
- CESRBDDs: binary decision diagrams with complemented edges and edge-specified reductions (2022)
- Behavioral Property Analysis and Supervisory Control of Petri Nets Using Semi-Structural Approaches (2022)
- Aggregation of clans to speed-up solving linear systems on parallel architectures (2022)
- Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems (2022)
- Using Approximation for the Verification of Token-Scaling Models (2022)
- Analyzing and Predicting Verification of Data-Aware Process Models–A Case Study With Spectrum Auctions (2022)
- Automata-Driven Partial Order Reduction and Guided Search for LTL Model Checking (2022)
- Bounded Model Checking for Unbounded Client-Server Systems (2022)
- Methods for Efficient Unfolding of Colored Petri Nets (2022)
- Portfolio Management in Explicit Model Checking (2022)
- Using Approximation for the Verification of Token-Scaling Models (2022)
- Petri-Net-Based Model Checking for Privacy-Critical Multiagent Systems (2022)
- Kong: a Tool to Squash Concurrent Places (2022)
- starMC: an automata based CTL* model checker (2022)
- Property Directed Reachability for Generalized Petri Nets (2022)
- Synthesis of Pure and Impure Petri nets With Restricted Place-environments: Complexity Issues (2021)
- Some Basic Techniques allowing Petri Net Synthesis: Complexity and Algorithmic Issues (2021)
- A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking (2021)
- Efficient Algorithms for Three Reachability Problems in Safe Petri Nets (2021)
- Skeleton Abstraction for Universal Temporal Properties (2021)
- Time For Stubborn Game Reductions (2021)
- The VLSAT-2 Benchmark Suite (2021)
- Extended abstract dependency graphs (2021)
- AALTITOAD A Tick Tock Automata Verification Engine (2021)
- Solving Finite-Linear-Path CTL-Formulas Using the CEGAR Approach (2021)
- The RERS challenge: towards controllable and scalable benchmark synthesis (2021)
- Maximal and minimal dynamic Petri net slicing (2021)
- A Method for Improving Memory Efficiency of the Reachability Graph Generation Process in General Petri Nets (2021)
- ZaligVinder: A generic test framework for string solvers (2021)
- Improving Explicit Model Checking for Petri Nets (2021)
- Petri Net Based CTL Model Checking: Using a New Method to Construct OBDD Variable Order (2021)
- Improvements in Unfolding of Colored Petri Nets (2021)
- The Reachability Problem for Acyclic Join-Free Petri nets is NP-complete (2021)
- Unfolding of Colored Petri Nets by Color Quotienting and Approximation (2021)
- Accelerating the Computation of Dead and Concurrent Places using Reductions (2021)
- Firing Partial Orders in a Petri Net (2021)
- Synthesis of Petri Nets with Restricted Place-Environments: Classical and Parameterized (2021)
- Skeleton Abstraction for Universal Temporal Properties (2021)
- Symbolic and Structural Model-Checking (2021)
- Efficient Algorithms for Three Reachability Problems in Safe Petri Nets (2021)
- A Lazy Query Scheme for Reachability Analysis in Petri Nets (2021)
- On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets (2021)
- Büchi-Automata guided Partial Order Reduction for LTL (2020)
- Unfolding of Coloured Petri Nets — Comparing the Runtime of two Approaches (2020)
- Efficient Strategies for CEGAR-Based Model Checking (2020)
- Symbolic Model Checking with Sentential Decision Diagrams (2020)
- A New Approach for the Symbolic Model Checking of Petri Nets (2020)
- Strategies, Model Checking and Branching-Time Properties in Maude (2020)
- AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (2020)
- The VLSAT-1 Benchmark Suite (2020)
- Proposal for Adding Useful Features to Petri-Net Model Checkers (2020)
- Petri Net Based Symbolic Model Checking for Computation Tree Logic of Knowledge (2020)
- Verification of Token-Scaling Models using an Under-Approximation (2020)
- Portfolio Management in Explicit Model Checking (2020)
- Faster Enabledness-Updates for the Reachability Graph Computation (2020)
- A CTL* Model Checker for Petri Nets (2020)
- Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams (2020)
- Modular Model Checking of Reference Nets: MoMoC (2020)
- Modeling the Raft Distributed Consensus Protocol in LNT (2020)
- MCC: a Tool for Unfolding Colored Petri Nets in PNML Format (2020)
- Unfolding of Coloured Petri Nets — Comparing the Runtime of two Approaches (2020)
- Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion (2020)
- Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account (2019)
- Efficient Learning and Analysis of System Behavior (2019)
- Can machine learning automatically choose your best model checking strategy? (2019)
- Variable order metrics for decision diagrams in system verification (2019)
- Solving E (φ U ψ) using the CEGAR Approach (2019)
- Generating Hard Benchmark Problems for Weak Bisimulation (2019)
- Saturation Enhanced with Conditional Locality: Application to Petri Nets (2019)
- Great-Nsolve: A Tool Integration for (Markov Regenerative) Stochastic Petri Nets (2019)
- RERS 2019: Combining Synthesis with Real-World Models (2019)
- Reflections on Bernhard Steffen’s Physics of Software Tools (2019)
- Witness generation in existential CTL model checking (2019)
- Experience Report on an Inquiry-Based Course on Model Checking (2019)
- Evaluation of model checkers by verifying message passing programs (2019)
- Software Architecture of Modern Model Checkers (2019)
- Taking Some Burden Off an Explicit CTL Model Checker (2019)
- Model Checking Data Flows in Concurrent Network Updates (2019)
- Can machine learning automatically choose your best model checking strategy? (2019)
- Model checking with generalized Rabin and Fin-less automata (2019)
- Improving Saturation Efficiency with Implicit Relations (2019)
- Saturation Enhanced with Conditional Locality: Application to Petri Nets (2019)
- Counting Petri net markings from reduction equations (2019)
- Binary Decision Diagrams with Edge-Specified Reductions (2019)
- Stubborn versus structural reductions for Petri nets (2019)
- Multi-core On-The-Fly Saturation (2019)
- Experience Report on An Inquiry-Based Course on Model Checking (2019)
- Abstract Dependency Graphs and Their Application to Model Checking (2019)
- TOOLympics 2019: An Overview of Competitions in Formal Methods (2019)
- The Rewrite Engines Competitions: A RECtrospective (2019)
- Nested-unit Petri nets (2019)
- RERS 2018: CTL, LTL, and Reachability (2018)
- Synthesizing Subtle Bugs with Known Witnesses (2018)
- Synthesizing Subtle Bugs with Known Witnesses (2018)
- Modeling and Analyzing Cyber Physical Systems Using High Level Petri Nets (2018)
- Petri Net Synthesis with Union/Find (2018)
- Simplification of CTL Formulae for Efficient Model Checking of Petri Nets (2018)
- Petri Net Reductions for Counting Markings (2018)
- Assessing SMT and CLP approaches for workflow nets verification (2018)
- Generation of Minimum Tree-Like Witnesses for Existential CTL (2018)
- Towards Reliable Benchmarks of Timed Automata (2018)
- Decision Diagrams for Petri Nets: A Comparison of Variable Ordering Algorithms (2018), (or here
- Petri Net Model Checking with LoLA 2 (2018)
- Self-adaptive Model Checking, the Next Step (2018)
- A Model Checker Collection for the Model Checking Contest Using Docker and Machine Learning (2018)
- A Distributed Fixed-Point Algorithm for Extended Dependency Graphs (2018)
- Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (2018)
- Generation of Minimum Tree-Like Witnesses for Existential CTL (2018)
- Gradient-based Variable Ordering of Decision Diagrams for Systems with Structural Units (2017)
- Property-Preserving Generation of Tailored Benchmark Petri Nets (2017)
- Explicit state model checking with generalized Büchi and Rabin automata (2017)
- A Method to Analyze Predicate Transition Nets Using SPIN Model Checker (2017)
- Stubborn Versus Structural Reductions for Petri Nets (2017)
- Property-Preserving Parallel Decomposition (2017)
- 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)
- Layered Data: A Modular Formal Definition without Formalisms (2016)
- 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)
- A Method of Sample Models of Program Construction in Terms of Petri Nets (2015)
- Génération de règles de coordination à partir de réseaux de Petri colorés (2015)
- 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)
- Vers l'intégration de paramètres temporels statiques et dynamiques dans les techniques de vérification par ordre partiel (2014)
- 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)