{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T21:10:23Z","timestamp":1781298623192,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642161636","type":"print"},{"value":"9783642161643","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16164-3_8","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T06:56:55Z","timestamp":1284965815000},"page":"106-123","source":"Crossref","is-referenced-by-count":22,"title":["Efficient Explicit-State Model Checking on General Purpose Graphics Processors"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damian","family":"Sulewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ceska, M., Lamr, T.: CUDA accelerated LTL model checking. In: International Conference on Parallel and Distributed Systems (ICPADS), pp. 34\u201341 (2009)","DOI":"10.1109\/ICPADS.2009.50"},{"key":"8_CR2","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":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"issue":"7","key":"8_CR4","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"B. Bloom","year":"1970","unstructured":"Bloom, B.: Space\/time trade-offs in hashing coding with allowable errors. Communication of the ACM\u00a013(7), 422\u2013426 (1970)","journal-title":"Communication of the ACM"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02652-2_7","volume-title":"Model Checking Software","author":"D. Bosnacki","year":"2009","unstructured":"Bosnacki, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol.\u00a05578, pp. 32\u201349. Springer, Heidelberg (2009)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","volume-title":"Formal Methods in Computer-Aided Design","author":"L. Brim","year":"2004","unstructured":"Brim, L., Cern\u00e1, I., Moravec, P., Simsa, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 352\u2013366. Springer, Heidelberg (2004)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1109\/ASPEC.2007.55","volume-title":"14th Asia-Pacific Software Engineering Conference (APSEC)","author":"F. Brizzolari","year":"2007","unstructured":"Brizzolari, F., Melatti, I., Tronci, E., Della Penna, G.: Disk based software verification via bounded model checking. In: 14th Asia-Pacific Software Engineering Conference (APSEC), pp. 358\u2013365. IEEE Computer Society, Los Alamitos (2007)"},{"issue":"46","key":"8_CR8","doi-asserted-by":"publisher","first-page":"53","DOI":"10.2307\/2001990","volume":"8","author":"A.W. Burks","year":"1954","unstructured":"Burks, A.W., Warren, D.W., Wright, J.B.: An analysis of a logical machine using parenthesis-free notation. Mathematical Tables and Other Aids to Computation\u00a08(46), 53\u201357 (1954)","journal-title":"Mathematical Tables and Other Aids to Computation"},{"key":"8_CR9","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":"8_CR10","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":"#cr-split#-8_CR11.1","unstructured":"Edelkamp, S., Sulewski, D.: Model checking via delayed duplicate detection on the GPU. Technical Report 821, Technische Universit??t Dortmund (2008);"},{"key":"#cr-split#-8_CR11.2","unstructured":"Presented on the 22nd Workshop on Planning, Scheduling, and Design PUK (2008)"},{"key":"8_CR12","unstructured":"Edelkamp, S., Sulewski, D.: Perfect hashing for domain-dependent planning on the GPU. In: 20th International Conference on Automated Planning and Scheduling (to appear, 2010)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-85114-1_8","volume-title":"Model Checking Software","author":"S. Evangelista","year":"2008","unstructured":"Evangelista, S.: Dynamic delayed duplicate detection for external memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 77\u201394. Springer, Heidelberg (2008)"},{"issue":"2","key":"8_CR14","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.ic.2006.10.003","volume":"205","author":"H. Gao","year":"2007","unstructured":"Gao, H., Hesselink, W.H.: A general lock-free algorithm using compare-and-swap. Inf. Comput.\u00a0205(2), 225\u2013241 (2007)","journal-title":"Inf. Comput."},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-540-73370-6_4","volume-title":"Model Checking Software","author":"P. Gastin","year":"2007","unstructured":"Gastin, P., Moro, P.: Minimal counterexample generation in SPIN. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 24\u201338. Springer, Heidelberg (2007)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Govindaraju, N.K., Gray, J., Kumar, R., Manocha, D.: GPUTeraSort: High performance graphics coprocessor sorting for large database management. In: International Conference on Management of Data (SIGMOD), pp. 325\u2013336 (2006)","DOI":"10.1145\/1142473.1142511"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-77220-0_21","volume-title":"High Performance Computing \u2013 HiPC 2007","author":"P. Harish","year":"2007","unstructured":"Harish, P., Narayanan, P.: Accelerating large graph algorithms on the gpu using cuda. In: Aluru, S., Parashar, M., Badrinath, R., Prasanna, V.K. (eds.) HiPC 2007. LNCS, vol.\u00a04873, pp. 197\u2013208. Springer, Heidelberg (2007)"},{"key":"8_CR18","volume-title":"GPU Gems 3","author":"M. Harris","year":"2007","unstructured":"Harris, M., Sengupta, S., Owens, J.D.: Parallel prefix sum (scan) with cuda. In: GPU Gems 3. Addison-Wesley, Reading (August 2007)"},{"key":"8_CR19","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2004","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"issue":"10","key":"8_CR20","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G. Holzmann","year":"2007","unstructured":"Holzmann, G., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Transactions on Software Engineering\u00a033(10), 659\u2013674 (2007)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design\u00a013(3), 287\u2013305 (1998)","journal-title":"Formal Methods in System Design"},{"issue":"6","key":"8_CR22","first-page":"164903","volume":"124","author":"G. Jayachandran","year":"2006","unstructured":"Jayachandran, G., Vishal, V., Pande, V.S.: Using massively parallel simulations and Markovian models to study protein folding: Examining the Villin head-piece. Journal of Chemical Physics\u00a0124(6), 164903\u2013164914 (2006)","journal-title":"Journal of Chemical Physics"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-85114-1_13","volume-title":"Model Checking Software","author":"P. Lamborn","year":"2008","unstructured":"Lamborn, P., Hansen, E.: Layered duplicate detection in external-memory model checking. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 160\u2013175. Springer, Heidelberg (2008)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Leischner, N., Osipov, V., Sanders, P.: Gpu sample sort. CoRR, abs\/0909.5649 (2009)","DOI":"10.1109\/IPDPS.2010.5470444"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-85114-1_17","volume-title":"Model Checking Software","author":"V.Y. Nguyen","year":"2008","unstructured":"Nguyen, V.Y., Ruys, T.C.: Incremental hashing for Spin. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 232\u2013249. Springer, Heidelberg (2008)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44676-1_10","volume-title":"Algorithms - ESA 2001","author":"R. Pagh","year":"2001","unstructured":"Pagh, R., Rodler, F.F.: Cuckoo hashing. In: Meyer auf der Heide, F. (ed.) ESA 2001. LNCS, vol.\u00a02161, pp. 121\u2013133. Springer, Heidelberg (2001)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"1781","DOI":"10.1002\/jcc.20289","volume":"26","author":"J.C. Phillips","year":"2005","unstructured":"Phillips, J.C., Braun, R., Wang, W., Gumbart, J., Tajkhorshid, E., Villa, E., Chipot, C., Skeel, R.D., Kale, L., Schulten, K.: Scalable molecular dynamics with NAMD. Journal of Computational Chemistry\u00a026, 1781\u20131802 (2005)","journal-title":"Journal of Computational Chemistry"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Putze, F., Sanders, P., Singler, J.: Cache-, hash-, and space-efficient bloom filters. ACM Journal of Experimental Algorithmics 14 (2009)","DOI":"10.1145\/1498698.1594230"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","first-page":"172","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1993","unstructured":"Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the murphi verifier. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 172\u2013183. Springer, Heidelberg (1993)"},{"key":"8_CR32","volume-title":"23rd IEEE International Symposium on Parallel and Distributed Processing (IPDPS)","author":"K. Verstoep","year":"2009","unstructured":"Verstoep, K., Bal, H., Barnat, J., Brim, L.: Efficient Large-Scale Model Checking. In: 23rd IEEE International Symposium on Parallel and Distributed Processing (IPDPS). IEEE, Los Alamitos (2009)"}],"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-16164-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,4]],"date-time":"2019-06-04T18:51:35Z","timestamp":1559674295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16164-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642161636","9783642161643"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16164-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}