BEEM: Benchmarks for Explicit Model Checker. We present Beem — BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 parametrized models (300 concrete instances) together with their correctness properties (both safety and liveness). The benchmark set is accompanied by an comprehensive web portal, which provides detailed information about all models. The web portal also includes information about state spaces and facilities for selection of models for experiments. The address of the web portal is

References in zbMATH (referenced in 30 articles )

Showing results 1 to 20 of 30.
Sorted by year (citations)

1 2 next

  1. Blahoudek, František; Major, Juraj; Strejček, Jan: LTL to self-loop alternating automata with generic acceptance and back (2020)
  2. Lammich, Peter: Refinement to imperative HOL (2019)
  3. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  4. Keiren, Jeroen J. A.: Benchmarks for parity games (2015) ioport
  5. Lammich, Peter: Refinement to Imperative/HOL (2015)
  6. López Bóbeda, Edmundo; Colange, Maximilien; Buchs, Didier: Stratagem: a generic Petri net verification framework (2014) ioport
  7. Blahoudek, František; Křetínský, Mojmír; Strejček, Jan: Comparison of LTL to deterministic Rabin automata translators (2013)
  8. Evangelista, Sami; Kristensen, Lars Michael: Dynamic state space partitioning for external memory state space exploration (2013) ioport
  9. Renault, Etienne; Duret-Lutz, Alexandre; Kordon, Fabrice; Poitrenaud, Denis: Strength-based decomposition of the property Büchi automaton for faster model checking (2013)
  10. Barnat, Jiří; Brim, Luboš; Ročkai, Petr: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties (2012)
  11. Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo: Exploiting step semantics for efficient bounded model checking of asynchronous systems (2012)
  12. Gaiser, Andreas; Křetínský, Jan; Esparza, Javier: Rabinizer: small deterministic automata for (\mathrmLTL(\mathrmF,\mathrmG)) (2012)
  13. Abdulla, Parosh Aziz; Chen, Yu-Fang; Clemente, Lorenzo; Holík, Lukáš; Hong, Chih-Duo; Mayr, Richard; Vojnar, Tomáš: Advanced Ramsey-based Büchi automata inclusion testing (2011)
  14. Edelkamp, S.; Sulewski, D.; Barnat, J.; Brim, L.; Šimeček, P.: Flash memory efficient LTL model checking (2011)
  15. Edelkamp, Stefan; Sulewski, Damian: External memory breadth-first search with delayed duplicate detection on the GPU (2011) ioport
  16. Evangelista, Sami; Petrucci, Laure; Youcef, Samir: Parallel nested depth-first searches for LTL model checking (2011)
  17. Barnat, J.; Brim, L.; Ročkai, P.: Scalable shared memory LTL model checking (2010) ioport
  18. Dubrovin, Jori: Checking bounded reachability in asynchronous systems by symbolic event tracing (2010)
  19. Evangelista, Sami; Pajault, Christophe: Solving the ignoring problem for partial order reduction (2010) ioport
  20. Weber, Michael: An embeddable virtual machine for state space generation (2010) ioport

1 2 next