{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:51:20Z","timestamp":1752983480233},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026515"},{"type":"electronic","value":"9783642026522"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02652-2_7","type":"book-chapter","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T11:43:06Z","timestamp":1245930186000},"page":"32-49","source":"Crossref","is-referenced-by-count":16,"title":["Efficient Probabilistic Model Checking on General Purpose Graphics Processors"],"prefix":"10.1007","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damian","family":"Sulewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","first-page":"112","volume-title":"Proc. 7th Int. Workshop on Petri Nets and Peformance Models (PNPM 1997)","author":"S.C. Allmaier","year":"1997","unstructured":"Allmaier, S.C., Kowarschik, M., Horton, G.: State Space Construction and Steady-state Solution of GSPNs on a Shared-Memory Multiprocessor. In: Proc. 7th Int. Workshop on Petri Nets and Peformance Models (PNPM 1997), pp. 112\u2013121. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"key":"7_CR2","first-page":"950","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking, p. 950. MIT Press, Cambridge (2008)"},{"issue":"6","key":"7_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Haverkort, B.: Model-Checking Algorithms for Contiuous-Time Markov Chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR4","unstructured":"Bal, H., Barnat, J., Brim, L., Verstoep, K.: Efficient Large-Scale Model Checking. In: IEEE International Parallel & Distributed Processing Symposium (IPDPS) (to appear, 2009)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-73370-6_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable Multi-core Model-Checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1109\/QEST.2008.29","volume-title":"International Conference on the Quantitative Evaluaiton of Systems QEST 2008","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Ceska, M., Tumova, J.: ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. In: International Conference on the Quantitative Evaluaiton of Systems QEST 2008, pp. 77\u201378. IEEE Compuer Society Press, Los Alamitos (2008)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-73368-3_32","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P.: I\/O efficient accepting cycle detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2001","unstructured":"Barnat, J., Brim, L., Str\u00edbrn\u00e1, J.: Distributed LTL Model Checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78800-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P., Weber, M.: Revisiting resistance speeds up I\/O-efficient LTL model checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 48\u201362. Springer, Heidelberg (2008)"},{"key":"7_CR10","unstructured":"Baskaran, M.M., Bordawekar, R.: Optimzing Sparse Matrix-Vector Multiplication on GPUs Using Compile-time and Run-time Strategies, IBM Reserach Report, RC24704, W0812-047 (2008)"},{"key":"7_CR11","first-page":"177","volume-title":"Formal Methods in System Design","author":"A. Bell","year":"2006","unstructured":"Bell, A., Haverkort, B.R.: Distribute Disk-based Algorithms for Model Checking Very Large Markov Chains. In: Formal Methods in System Design, vol.\u00a029, pp. 177\u2013196. Springer, Heidelberg (2006)"},{"key":"7_CR12","first-page":"344","volume":"2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G.: Distributed and Structured Analysis Approaches to Study Large and Complex Systems. European Educational Forum: School on Formal Methods and Performance Analysis\u00a02000, 344\u2013374 (2000)","journal-title":"European Educational Forum: School on Formal Methods and Performance Analysis"},{"key":"7_CR13","unstructured":"Dai, P., Mausam, Weld, D.S.: External Memory Value Iteration. In: Proc. of the Twenty-Third AAAI Conf. on Artificial Intelligence (AAAI), pp. 898\u2013904 (2008)"},{"key":"7_CR14","unstructured":"http:\/\/www.nvidia.com\/object\/cuda_home.html#"},{"key":"7_CR15","unstructured":"Edelkamp, S., Sulewski, D.: Model Checking via Delayed Duplicate Detection on the GPU, Technical Report 821, Universit\u00e4t Dortmund, Fachberich Informatik, ISSN 0933-6192 (2008)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"7_CR17","first-page":"128","volume-title":"Proc. 17th Int. Conf. on Automated Planning and Scheduling","author":"S. Edelkamp","year":"2007","unstructured":"Edelkamp, S., Jabbar, S., Bonet, B.: External Memory Value Iteration. In: Proc. 17th Int. Conf. on Automated Planning and Scheduling, pp. 128\u2013135. AAAI Press, Menlo Park (2007)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-70545-1_50","volume-title":"Computer Aided Verification","author":"S. Edelkamp","year":"2008","unstructured":"Edelkamp, S., Sanders, P., \u0160ime\u010dek, P.: Semi-external LTL model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 530\u2013542. Springer, Heidelberg (2008)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: Software Engineering and Formal Methods, pp. 73\u201382 (2008)","DOI":"10.1109\/SEFM.2008.34"},{"issue":"5","key":"7_CR20","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A Logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Haverkort, B., Hermanns, H., Katoen, J.-P.: On the Use of Model Checking Techniques for Dependability Evaluation. In: Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS 2000), pp. 228\u2013237 (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"issue":"2","key":"7_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T. Herman","year":"1990","unstructured":"Herman, T.: Probabilistic Self-stabilization. Information Processing Letters\u00a035(2), 63\u201367 (1990)","journal-title":"Information Processing Letters"},{"key":"7_CR23","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In: Proc. 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188\u2013207 (1999)"},{"issue":"10","key":"7_CR24","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: The Design of a multi-core extension of the Spin Model Checker. IEEE Trans. on Software Engineering\u00a033(10), 659\u2013674 (2007); (first presented at: Formal Methods in Computer Aided Design (FMCAD), San Jose (November 2006))","journal-title":"IEEE Trans. on Software Engineering"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: Multi-core Model Checking with Spin. In: Proc. Parallel and Distributed Processing Symposium, IPDPS 2007, IEEE International, pp. 1\u20138 (2007)","DOI":"10.1109\/IPDPS.2007.370410"},{"issue":"4","key":"7_CR26","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2004.10.022","volume":"128","author":"C.P. Inggs","year":"2005","unstructured":"Inggs, C.P., Barringer, H.: CTL* Model Checking on a Shared Memory Architecture. Electronic Notes in Theoretical Computer Science\u00a0128(4), 107\u2013123 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Inggs, C.P., Barringer, H.: Effective State Exploration for Model Checking on a Shared Memory Architecture. Electronic Notes in Theoretical Computer Science\u00a068(4) (2002)","DOI":"10.1016\/S1571-0661(05)80395-0"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M.Z. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed Model Checking in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 22\u201339. Springer, Heidelberg (1999)"},{"issue":"9","key":"7_CR31","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1284621.1284622","volume":"50","author":"A. Marowka","year":"2007","unstructured":"Marowka, A.: Parallel Computing on Any Desktop. Comm. of the ACM\u00a050(9), 75\u201378 (2007)","journal-title":"Comm. of the ACM"},{"key":"7_CR32","doi-asserted-by":"publisher","first-page":"1781","DOI":"10.1002\/jcc.20289","volume":"26","author":"J.C. Philips","year":"2005","unstructured":"Philips, J.C., Braun, R., Wang, W., Gumbart, J., Tajkhorshid, E., Villa, E., Chipot, C., Skeel, R.D., Kale, L., Sculten, K.: Scalable Molecular Dynamics with NAMD. Journal of Computational Chemistry\u00a026, 1781\u20131802 (2005)","journal-title":"Journal of Computational Chemistry"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Stern, U., Dill, D.: Parallelizing the Mur\u03c6 Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"7_CR34","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/3-540-65306-6_21","volume-title":"Lectures on Petri Nets I: Basic Models","author":"A. Valmari","year":"1998","unstructured":"Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol.\u00a01491, pp. 429\u2013528. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02652-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T23:55:39Z","timestamp":1552089339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02652-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026515","9783642026522"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02652-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}