BEEM: References

• Examples of applications of BEEM (for fuller list see Google Scholar):
  • Incremental Hashing for SPIN. Nguyen, Ruys. SPIN 2008.
  • Model Classifications and Automated Verification. R. Pelanek. FMICS 2007.
  • Scalable Multi-Core LTL Model-Checking. J. Barnat, L. Brim, P. Rockai. SPIN 2007.
  • I/O Efficient Accepting Cycle Detection. J. Barnat, L. Brim, P. Simecek. CAV 2007.
  • Some Solutions to the Ignoring Problem. S. Evangelista and C. Pajault. SPIN 2007.
  • Shared Hash Tables in Parallel Model Checking. J. Barnat and P. Rockai. PDMC 2007.
  • Mechanizing the Powerset Construction for Restricted Classes of omega-Automata. C. Dax, J. Eisinger, F. Klaedtke. ATVA 2007.
  • Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. J. Barnat, L. Brim, P. Simecek and M. Weber. TACAS 2008.
  • Complementarity of Error Detection Techniques. R. Pelanek, V. Rosecky, P. Moravec. PDMC 2008.
  • Evaluation of State Caching and State Compression Techniques. R. Pelanek, V. Rosecky, J. Sedenka. Technical report FIMU-RS-2008-02.
  • Estimating State Space Parameters. R. Pelanek, P. Simecek. Technical report FIMU-RS-2008-01.
  • Producing short counterexamples using "crucial events". S. Kashyap and V. K. Garg.
  • Multi-Threaded Nested DFS. P. Rockai.
  • Motifs in State Spaces. J. Krcal.
  • Optimising Techniques for Model Checkers. Viet Yen Nguyen.
  • Vergleich von Algorithmen fur den Leerheitstest von Buchiautomaten. A. Gaiser.
• Tools:
  • DiVinE (The Distributed Verification Environment) - An extensible model checking environment supporting the DVE language.
  • Yahoda - Database of verification tools
• Other benchmarks and model collections:
  • VLTS suite
  • Example Repository for Finite State Verification Tools
  • Promela model database
  • CADP case studies