1. A. Aggarwal & J. S. Vitter (1988): The input/output complexity of sorting and related problems. Communications of the ACM 31(9), pp. 1116–1127.
  2. S. Allmaier, S. Dalibor & D. Kreische (1997): Parallel Graph Generation Algorithms for Shared and Distributed Memory Machines. In: G. Bilardi, A. G. Ferreira, R. Lüling & J. D. P. Rolim: Proceeding of the Parallel Computing Conference PARCO'97 (Bonn, Germany), LNCS 1253. Springer, pp. 207–218. Available at
  3. Tonglaga Bao & Michael Jones (2005): Time-Efficient Model Checking with Magnetic Disk. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), LNCS 3440. Springer, pp. 526–540, doi:10.1007/978-3-540-31980-1_34.
  4. J. Barnat (2004): Distributed Memory LTL Model Checking. Masaryk University Brno, Faculty of Informatics. Available at
  5. J. Barnat, P. Bauch, L. Brim & M. Češka (2010): Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In: 16th International Conference on Parallel and Distributed Systems (ICPADS 2010). IEEE Computer Society, pp. 259–266, doi:10.1109/ICPADS.2010.82.
  6. J. Barnat, P. Bauch, L. Brim & M. Češka (2011): Computing Strongly Connected Components in Parallel on CUDA. In: International Parallel & Distributed Processing Symposium (IPDPS'11). IEEE Computer Society, pp. 541–552, doi:10.1109/IPDPS.2011.59.
  7. J. Barnat, L. Brim & I. Černá (2002): Property driven distribution of Nested DFS. In: Proc. Workshop on Verification and Computational Logic, DSSE Technical Report DSSE-TR-2002-5. University of Southampton, UK, pp. 1–10. Available at
  8. J. Barnat, L. Brim & J. Chaloupka (2003): Parallel Breadth-First Search LTL Model-Checking. In: 18th IEEE International Conference on Automated Software Engineering (ASE'03). IEEE Computer Society, pp. 106–115, doi:10.1109/ASE.2003.1240299.
  9. J. Barnat, L. Brim & J. Chaloupka (2005): From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronic Notes in Theoretical Computer Science 133(1), pp. 21–39, doi:10.1016/j.entcs.2004.08.056.
  10. J. Barnat, L. Brim & P. Ročkai (2007): Scalable Multi-core LTL Model-Checking. In: Model Checking Software, LNCS 4595. Springer, pp. 187–203, doi:10.1007/978-3-540-73370-6_13.
  11. J. Barnat, L. Brim & P. Ročkai (2008): DiVinE Multi-Core – A Parallel LTL Model-Checker. In: Automated Technology for Verification and Analysis (ATVA 2008), LNCS 5311. Springer, pp. 234–239, doi:10.1007/978-3-540-88387-6_20.
  12. J. Barnat, L. Brim & P. Ročkai (2009): A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In: Formal Methods and Software Engineering (ICFEM 2009), LNCS 5885. Springer, pp. 407–425, doi:10.1007/978-3-642-10373-5_21.
  13. J. Barnat, L. Brim & P. Ročkai (2010): Parallel Partial Order Reduction with Topological Sort Proviso. In: Software Engineering and Formal Methods (SEFM 2010). IEEE Computer Society Press, pp. 222–231, doi:10.1109/SEFM.2010.35.
  14. J. Barnat, L. Brim & J. Stř\'ıbrná (2001): Distributed LTL Model-Checking in SPIN. In: Proc. SPIN Workshop on Model Checking of Software, LNCS 2057. Springer, pp. 200–216, doi:10.1007/3-540-45139-0_13.
  15. J. Barnat, L. Brim, I. Černá, P. Moravec, P. Ročkai & P. Šimeček (2006): DiVinE – A Tool for Distributed Verification (Tool Paper). In: Computer Aided Verification, LNCS 4144/2006. Springer Berlin / Heidelberg, pp. 278–281, doi:10.1007/11817963_26.
  16. J. Barnat, L. Brim & M. Češka (2009): DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science (PDMC 2009) 14, pp. 107–111, doi:10.4204/EPTCS.14.8.
  17. J. Barnat, L. Brim, M. Češka & T. Lamr (2009): CUDA accelerated LTL Model Checking. In: 15th International Conference on Parallel and Distributed Systems (ICPADS 2009). IEEE Computer Society, pp. 34–41, doi:10.1109/ICPADS.2009.50.
  18. J. Barnat, L. Brim, M. Češka & P. Ročkai (2010): DiVinE: Parallel Distributed Model Checker (Tool paper). In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010). IEEE, pp. 4–7, doi:10.1109/PDMC-HiBi.2010.9.
  19. J. Barnat, L. Brim & P. Šimeček (2007): I/O Efficient Accepting Cycle Detection. In: Computer Aided Verification, LNCS 4590. Springer, pp. 281–293, doi:10.1007/978-3-540-73368-3_32.
  20. J. Barnat, L. Brim, P. Šimeček & M. Weber (2008): Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS)., LNCS 4963. Springer, pp. 48–62, doi:10.1007/978-3-540-78800-3_5.
  21. J. Barnat & P. Ročkai (2008): Shared Hash Tables in Parallel Model Checking. ENTCS 198(1), pp. 79–91, doi:10.1016/j.entcs.2007.10.021.
  22. G. Behrmann, T. S. Hune & F. W. Vaandrager (2000): Distributed Timed Model Checking — How the Search Order Matters. In: Proc. 12th Conference on Computer-Aided Verification CAV00, LNCS 1855. Springer, pp. 216–231, doi:10.1007/10722167_19.
  23. Armin Biere, Cyrille Artho & Viktor Schuppan (2002): Liveness Checking as Safety Checking. Electronic Notes in Theoretical Computer Science 66(2), pp. 160 – 177, doi:10.1016/S1571-0661(04)80410-9.
  24. Brad Bingham, Jesse Bingham, Flavio M. de Paula, John Erickson, Gaurav Singh & Mark Reitblatt (2010): Industrial Strength Distributed Explicit State Model Checking. In: Parallel and Distributed Methods in Verification, 2010 Ninth International Workshop on, and High Performance Computational Systems Biology, Second International Workshop on. IEEE Computer Society, pp. 28–36, doi:10.1109/PDMC-HiBi.2010.13.
  25. D. Bosnacki, S. Edelkamp & D. Sulewski (2009): Efficient Probabilistic Model Checking on General Purpose Graphics Processors. In: Model Checking Software (SPIN 2009), LNCS 5578. Springer, pp. 32–49, doi:10.1007/978-3-642-02652-2_7.
  26. L. Brim, I. Černá & L. Hejtmánek (2003): Parallel Algorithms for Detection of Negative Cycles. Technical Report FIMU-RS-2003-04. Faculty of Informatics, Masaryk University Brno. Available at
  27. L. Brim, I. Černá, P. Moravec & J. Šimša (2004): Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In: Formal Methods in Computer Aided Design (FMCAD), LNCS 4144. Springer, pp. 352–366, doi:10.1007/978-3-540-30494-4_25.
  28. L. Brim, I. Černá, P. Krčál & R. Pelánek (2001): Distributed LTL Model Checking Based on Negative Cycle Detection. In: Proc. of Foundations of Software Technology and Theoretical Computer Science (FST TCS 2001), LNCS 2245. Springer, pp. 96–107, doi:10.1007/3-540-45294-X_9.
  29. J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill & L. J. Hwang (1992): Symbolic Model Checking: 10^20 States and Beyond. Information and Computation 98(2), pp. 142–170. Available at
  30. S. Caselli, G. Conte & P. Marenzoni (1995): Parallel state space exploration for GSPN models. In: G. de Michelis & M. Diaz: Applications and Theory of Petri Nets 1995, LNCS 935. Springer Verlag, pp. 181–200, doi:10.1007/3-540-60029-9_40.
  31. I. Černá & R. Pelánek (2003): Distributed Explicit Fair Cycle Detection. In: Model Checking Software, 10th International SPIN Workshop, LNCS 2648. Springer, pp. 49–73, doi:10.1007/3-540-44829-2_4.
  32. I. Černá & R. Pelánek (2003): Relating Hierarchy of Temporal Properties to Model Checking. In: Mathematical Foundations of Computer Science (MFCS), LNCS 2747. Springer, pp. 318–327, doi:10.1007/978-3-540-45138-9_26.
  33. Yi-Jen Chiang, Michael T. Goodrich, Edward F. Grove, Roberto Tamassia, Darren Erik Vengroff & Jeffrey Scott Vitter (1995): External-memory graph algorithms. In: soda. Society for Industrial and Applied Mathematics, pp. 139–149, doi:10.1145/313651.313681.
  34. G. Ciardo, J. Gluckman & D.M. Nicol (1998): Distributed State Space Generation of Discrete-State Stochastic Models. INFORMS Journal on Computing 10(1), pp. 82–93, doi:10.1287/ijoc.10.1.82.
  35. Gianfranco Ciardo (1997): Automated parallelization of discrete state-space generation. J. Parallel Distrib. Comput. 47, pp. 153–167, doi:10.1006/jpdc.1997.1409.
  36. E. M. Clarke, R. Enders, T. Filkorn & S. Jha (1996): Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1-2), pp. 77–104, doi:10.1007/BF00625969.
  37. E.M. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2001): Progress on the State Explosion Problem in Model Checking. In: R. Wilhelm: Informatics - 10 Years Back. 10 Years Ahead, LNCS 2000. Springer, pp. 176–194.
  38. (2009): NVIDIA CUDA Compute Unified Device Architecture - Programming Guide Version 2.0,., June 2009.
  39. David L. Dill (1996): The Murφ verification system. In: Conference on Computer-Aided Verification (CAV'96), LNCS. Springer-Verlag, pp. 390–393. Available at
  40. Stefan Edelkamp, Peter Sanders & Pavel Šimeček (2008): Semi-external LTL Model Checking. In: Computer Aided Verification (CAV 2008). Springer, Berlin, Heidelberg, pp. 530–542, doi:10.1007/978-3-540-70545-1_50.
  41. Stefan Edelkamp & Damian Sulewski (2008): Model Checking via Delayed Duplicate Detection on the GPU.. Technical Report Technical Report 821. TU Dortmund. Available at Presented on the 22nd Workshop on Planning, Scheduling, and Design PUK 2008.
  42. Stefan Edelkamp & Damian Sulewski (2009): Parallel State Space Search on the GPU. Available at International Symposium on Combinatorial Search (SoCS 2009).
  43. T. von Eicken, D. E. Culler, S. C. Goldstein & K. E. Schauser (1992): Active messages: a mechanism for integrated communication and computation. In: 19th Annual International Symposium on Computer Architecture, pp. 256–266, doi:10.1145/285930.286002.
  44. E. Allen Emerson & A. Prasad Sistla (1996): Symmetry and model checking. Form. Methods Syst. Des. 9(1-2), pp. 105–131, doi:10.1007/BF00625970.
  45. Sami Evangelista (2008): Dynamic Delayed Duplicate Detection for External Memory Model Checking. In: SPIN '08: Proc. of the 15th international workshop on Model Checking Software. Springer, Berlin, Heidelberg, pp. 77–94, doi:10.1007/978-3-540-85114-1_8.
  46. H. Garavel, R. Mateescu & I.M Smarandache (2001): Parallel State Space Construction for Model-Checking. In: Matthew B. Dwyer: Model Checking of Software (SPIN'2001), LNCS 2057. Springer-Verlag, pp. 216–234, doi:10.1007/3-540-45139-0_14.
  47. Jaco Geldenhuys & P. J. A. de Villiers (1999): Runtime Efficient State Compaction in SPIN. In: SPIN, pp. 12–21, doi:10.1007/3-540-48234-2_2.
  48. Naga K. Govindaraju, Jim Gray, Ritesh Kumar & Dinesh Manocha (2006): GPUTeraSort: high performance graphics co-processor sorting for large database management. In: International Conference on Management of Data (SIGMOD 06). ACM, pp. 325–336, doi:10.1145/1142473.1142511.
  49. Moritz Hammer & Michael Weber (2006): "To Store or Not To Store" Reloaded: Reclaiming Memory on Demand. In: Formal Methods: Applications and Technology, LNCS 4346. Springer, pp. 51–66, doi:10.1007/978-3-540-70952-7_4.
  50. P. Harish & P. J. Narayanan (2007): Accelerating Large Graph Algorithms on the GPU Using CUDA. In: HiPC, LNCS 4873. Springer, pp. 197–208, doi:10.1007/978-3-540-77220-0_21.
  51. P. Harish, V. Vineet & P. J. Narayanan (2009): Large Graph Algorithms for Massively Multithreaded Architectures. Technical Report IIIT/TR/2009/74. Center for Visual Information Technology, International Institute of Information Technology Hyderabad, INDIA. Available at
  52. M. Harris: Optimizing Parallel Reduction in CUDA,., March 2010.
  53. B. R. Haverkort, A. Bell & H. C. Bohnenkamp (1999): On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets.. In: Petri Net and Performance Models (PNPM'99). IEEE Computer Society Press, pp. 12–21, doi:10.1109/PNPM.1999.796528.
  54. Boudewijn R. Haverkort, Henrik Bohnenkamp & Alexander Bell (1998): Efficiency Improvements in the Evaluation of Large Stochastic Petri Nets. In: Forschungsbericht: 5. Workshop Algorithmen und Werkzeuge f\IeC ür Petrinetze. Universit\IeC ät Dortmund, Fachbereich Informatik, pp. 55–61. Available at
  55. Keijo Heljanko, Victor Khomenko & Maciej Koutny (2002): Parallelisation of the Petri Net Unfolding Algorithm. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002), LNCS 2280. Springer, pp. 371–385, doi:10.1007/3-540-46002-0_26.
  56. Gerard J. Holzmann (2003): The Spin Model Checker: Primer and Reference Manual. Addison-Wesley.
  57. Gerard J. Holzmann (2008): A Stack-Slicing Algorithm for Multi-Core Model Checking. ENTCS 198(1), pp. 3–16, doi:10.1016/j.entcs.2007.10.017.
  58. Gerard J. Holzmann & Dragan Bosnacki (2007): The Design of a Multicore Extension of the SPIN Model Checker. IEEE Trans. Software Eng. 33(10), pp. 659–674, doi:10.1109/TSE.2007.70724.
  59. iFEST: Integration Framework for Embedded Systems Tools. Available at
  60. Cornelia P. Inggs & Howard Barringer (2005): CTL^* Model Checking on a Shared-Memory Architecture. Electronic Notes in Theoretical Computer Science 128(3), pp. 107–123, doi:10.1016/j.entcs.2004.10.022.
  61. Shahid Jabbar & Stefan Edelkamp (2005): I/O Efficient Directed Model Checking. In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2005), LNCS 3385. Springer, pp. 313–329, doi:10.1007/978-3-540-30579-8_21.
  62. Shahid Jabbar & Stefan Edelkamp (2006): Parallel External Directed Model Checking with Linear I/O. In: Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), LNCS 3855. Springer, pp. 237–251, doi:10.1007/11609773_16.
  63. G. Jayachandran, V. Vishal & V. S. Pande (2006): Using massively parallel simulations and Markovian models to study protein folding: examining the villin head-piece. Journal of Chemical Physics 124(6), pp. 903\IeC 914, doi:10.1063/1.2186317.
  64. Michael Jones & Eric Mercer (2004): Explicit State Model Checking with Hopper. In: Model Checking Software (SPIN 2004), Lecture Notes in Computer Science 2989. Springer, pp. 146–150, doi:10.1007/978-3-540-24732-6_10.
  65. A. B. Kahn (1962): Topological sorting of large networks. Communications of the ACM 5(11), pp. 558–562.
  66. W. Knottenbelt, P.G Harrison, M. Mestern & P.S. Kritzinger (2000): A Probabilistic Dynamic Technique for the Distributed Generation of Very Large State Spaces. Performance Evaluation 35(1–4), pp. 127–148, doi:10.1016/S0166-5316(99)00061-9.
  67. W. Knottenbelt, M. Mestern, P.G Harrison & P.S. Kritzinger (1998): Probability, Parallelism and the State Space Exploration Problem. In: R. Puigjaner: Tools'98, LNCS 1469. Springer Verlag, pp. 165–179, doi:10.1007/3-540-68061-6_14.
  68. R. Korf (2004): Best-First Frontier Search with Delayed Duplicate Detection. In: AAAI'04. AAAI Press / The MIT Press, pp. 650–657. Available at
  69. R. Korf & P. Schultze (2005): Large-Scale Parallel Breadth-First Search. In: Proceedings of the 20th national conference on Artificial intelligence - Volume 3. AAAI Press / The MIT Press, pp. 1380–1385. Available at
  70. Rahul Kumar & Eric G. Mercer (2005): Load Balancing Parallel Explicit State Model Checking. Electronic Notes in Theoretical Computer Science 128(3), pp. 19–34, doi:10.1016/j.entcs.2004.10.016.
  71. Alfons Laarman, Jaco van de Pol & Michael Weber (2010): Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Formal Methods in Computer-Aided Design (FMCAD 2010). IEEE, pp. 247–255. Available at
  72. Peter Lamborn & Eric A. Hansen (2008): Layered Duplicate Detection in External-Memory Model Checking. In: SPIN '08: Proc. of the 15th international workshop on Model Checking Software. Springer, Berlin, Heidelberg, pp. 160–175, doi:10.1007/978-3-540-85114-1_13.
  73. Flavio Lerda & Riccardo Sisto (1999): Distributed-memory Model Checking with SPIN. In: Proc. of the 5th International SPIN Workshop, LNCS 1680. Springer-Verlag, pp. 22–39, doi:10.1007/3-540-48234-2_3.
  74. Flavio Lerda & Willem Visser (2001): Addressing Dynamic Issues of Program Model Checking. In: International SPIN Workshop on Model Checking of Software (SPIN'2001), LNCS 2057. Springer, pp. 80–102, doi:10.1007/3-540-45139-0_6.
  75. Ulrich Meyer, Peter Sanders & Jop Sibeyn (2003): Algorithms for Memory Hierarchies. Springer.
  76. Doron Peled (1998): Ten Years of Partial Order Reduction. In: Proceedings of the 10th International Conference on Computer Aided Verification. Springer-Verlag, pp. 17–28.
  77. R. Pel\IeC ánek (2009): Fighting State Space Explosion: Review and Evaluation. In: Formal Methods for Industrial Critical Systems (FMICS 2008), LNCS 5596. Springer, pp. 37–52, doi:10.1007/978-3-642-03240-0_7.
  78. Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci & Marisa Venturini Zilli (2002): Exploiting Transition Locality in the Disk Based Murφ Verifier. In: Formal Methods in Computer-Aided Design (FMCAD 2002), pp. 202–219, doi:10.1007/3-540-36126-X_13.
  79. U. Stern & D. L. Dill (1997): Parallelizing the Murφ Verifier. In: O. Grumberg: Proceedings of Computer Aided Verification (CAV '97), LNCS 1254. Springer-Verlag, pp. 256–267, doi:10.1007/BFb0028727.
  80. U. Stern & D. L. Dill (1998): Using Magnetic Disk Instead of Main Memory in the Murφ Verifier. In: Computer Aided Verification. 10th International Conference, pp. 172–183, doi:10.1007/BFb0028743.
  81. M.Y. Vardi & P. Wolper (1986): An automata-theoretic approach to automatic program verification. In: Proc. IEEE Symposium on Logic in Computer Science. Computer Society Press, pp. 322–331.
  82. K. Verstoep, H. Bal, J. Barnat & L. Brim (2009): Efficient Large-Scale Model Checking. In: 23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009). IEEE, pp. 1–12, doi:10.1109/IPDPS.2009.5161000.
  83. Rong Zhou & Eric A. Hansen (2004): Structured Duplicate Detection in External-Memory Graph Search. In: AAAI. AAAI Press / The MIT Press, pp. 683–689. Available at

Comments and questions to:
For website issues: