References

  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 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.2006&rep=rep1&type=pdf.
  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 http://anna.fi.muni.cz/papers/src/public/74925f5d8351a5a41120c11f26f3a21b.pdf.
  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 http://anna.fi.muni.cz/papers/src/public/5f773c95a13c7b85f303123b36985210.pdf.
  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 http://www.fi.muni.cz/informatics/reports/files/2003/FIMU-RS-2003-04.pdf.
  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 http://citeseer.nj.nec.com/burch92symbolic.html.
  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,. http://www.nvidia.com/object/cuda_develop.html, 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 http://dl.acm.org/citation.cfm?id=647765.735832.
  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 http://www.tzi.de/~edelkamp/GPU_Technical.pdf. 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 http://www.cs.ualberta.ca/~nathanst/sara/papers/socs09_submission_24.pdf. 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 http://cvit.iiit.ac.in/papers/pawan09GraphAlgorithms.pdf.
  52. M. Harris: Optimizing Parallel Reduction in CUDA,. http://developer.download.nvidia.com/compute/cuda/1_1/Website/projects/reduction/doc/reduction.pdf, 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 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.41.3435&rep=rep1&type=pdf.
  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 http://www.artemis-ifest.eu.
  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 http://dl.acm.org/citation.cfm?id=1597148.1597253.
  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 http://dl.acm.org/citation.cfm?id=1619499.1619555.
  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 http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5770956.
  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 http://www.aaai.org/Papers/AAAI/2004/AAAI04-108.pdf.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org