{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:17:45Z","timestamp":1781075865448,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642206733","type":"print"},{"value":"9783642206740","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-20674-0_2","type":"book-chapter","created":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T06:06:05Z","timestamp":1303279565000},"page":"12-31","source":"Crossref","is-referenced-by-count":7,"title":["External Memory Breadth-First Search with Delayed Duplicate Detection on the GPU"],"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":"2_CR1","doi-asserted-by":"crossref","unstructured":"Ajwani, D., Dementiev, R., Meyer, U.: A computational study of external-memory BFS algorithms. In: ACM-SIAM Symposium On Discrete Algorithms (SODA), pp. 601\u2013610 (2006)","DOI":"10.1145\/1109557.1109623"},{"key":"2_CR2","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 LTL model-checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"107","DOI":"10.4204\/EPTCS.14.8","volume":"14","author":"J. Barnat","year":"2009","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M.: DiVinE-CUDA: A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science (PDMC)\u00a014, 107\u2013111 (2009)","journal-title":"Electronic Proceedings in Theoretical Computer Science (PDMC)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010ce\u0161ka, M., Lamr, T.: CUDA accelerated LTL Model Checking. In: International Conference on Parallel and Distributed Systems (ICPADS 2009), pp. 34\u201341 (2009)","DOI":"10.1109\/ICPADS.2009.50"},{"key":"2_CR5","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":"2_CR6","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":"2_CR7","first-page":"307","volume":"32","author":"K.E. Batcher","year":"1968","unstructured":"Batcher, K.E.: Sorting networks and their applications. AFIPS Spring Joint Computing Conference\u00a032, 307\u2013314 (1968)","journal-title":"AFIPS Spring Joint Computing Conference"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-04128-0_61","volume-title":"Algorithms - ESA 2009","author":"D. Belazzougui","year":"2009","unstructured":"Belazzougui, D., Botelho, F.C., Dietzfelbinger, M.: Hash, displace, and compress. In: Fiat, A., Sanders, P. (eds.) ESA 2009. LNCS, vol.\u00a05757, pp. 682\u2013693. Springer, Heidelberg (2009)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"1141","DOI":"10.2307\/2318556","volume":"80","author":"D. Bloom","year":"1973","unstructured":"Bloom, D.: A birthday problem. American Mathematical Monthly\u00a080, 1141\u20131142 (1973)","journal-title":"American Mathematical Monthly"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Botelho, F.C., Ziviani, N.: External perfect hashing for very large key sets. In: ACM Conference on Information and Knowledge Management (CIKM), pp. 653\u2013662 (2007)","DOI":"10.1145\/1321440.1321532"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Brizzolari, F., Melatti, I., Tronci, E., Penna, G.D.: Disk based software verification via bounded model checking. In: Asia-Pacific Software Engineering Conference (APSEC), pp. 358\u2013365 (2007)","DOI":"10.1109\/ASPEC.2007.55"},{"issue":"46","key":"2_CR12","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":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-87744-8_21","volume-title":"Algorithms - ESA 2008","author":"D. Cederman","year":"2008","unstructured":"Cederman, D., Tsigas, P.: A practical quicksort algorithm for graphics processors. In: Halperin, D., Mehlhorn, K. (eds.) Esa 2008. LNCS, vol.\u00a05193, pp. 246\u2013258. Springer, Heidelberg (2008)"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0166-218X(92)90127-V","volume":"37\/38","author":"G. Cooperman","year":"1992","unstructured":"Cooperman, G., Finkelstein, L.: New methods for using Cayley graphs in interconnection networks. Discrete Applied Mathematics\u00a037\/38, 95\u2013118 (1992)","journal-title":"Discrete Applied Mathematics"},{"key":"2_CR15","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":"2_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-30221-6_18","volume-title":"KI 2004: Advances in Artificial Intelligence","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Jabbar, S., Schr\u00f6dl, S.: External A*. In: Biundo, S., Fr\u00fchwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol.\u00a03238, pp. 226\u2013240. Springer, Heidelberg (2004)"},{"key":"2_CR17","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":"2_CR18","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: International Conference on Software Engineering and Formal Methods (SEFM), pp. 73\u201382 (2008)","DOI":"10.1109\/SEFM.2008.34"},{"key":"2_CR19","unstructured":"Edelkamp, S., Sulewski, D.: Model checking via delayed duplicate detection on the GPU. Technical Report 821, Technische Universit\u00e4t Dortmund. Presented on the 22nd Workshop on Planning, Scheduling, and Design PUK 2008 (2008)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D., Y\u00fccel, C.: Perfect hashing for domain-dependent planning on the gpu. In: International Conference on Automated Planning and Scheduling, ICAPS (2010) (to appear)","DOI":"10.1609\/icaps.v20i1.13414"},{"key":"2_CR21","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 for SPIN. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 24\u201338. Springer, Heidelberg (2007)"},{"key":"2_CR22","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":"2_CR23","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":"3","key":"2_CR24","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"},{"key":"2_CR25","unstructured":"Jabbar, S.: External Memory Algorithms for State Space Exploration in Model Checking and Action Planning. PhD thesis, Technical University of Dortmund (2008)"},{"key":"2_CR26","volume-title":"The Art of Computer Programming","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming. Addison-Wesley, Reading (1973)"},{"key":"2_CR27","unstructured":"Korf, R.: Delayed duplicate detection: extended abstract. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1539\u20131541 (2003)"},{"key":"2_CR28","unstructured":"Korf, R.: Best-first frontier search with delayed duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 650\u2013657 (2004)"},{"key":"2_CR29","unstructured":"Korf, R., Felner, A.: Recent progress in heuristic search: A case study of the Four-Peg Towers of Hanoi problem. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 2334\u20132329 (2007)"},{"key":"2_CR30","unstructured":"Korf, R., Schultze, P.: Large-scale parallel breadth-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 1380\u20131385 (2005)"},{"key":"2_CR31","unstructured":"Korf, R.E.: Breadth-first frontier search with delayed duplicate detection. In: MOCHART, pp. 87\u201392 (2003)"},{"key":"2_CR32","unstructured":"Korf, R.E.: Minimizing disk I\/O in two-bit-breath-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 317\u2013324 (2008)"},{"key":"2_CR33","unstructured":"Korf, R.E., Schultze, T.: Large-scale parallel breadth-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 1380\u20131385 (2005)"},{"key":"2_CR34","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. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 160\u2013175. Springer, Heidelberg (2008)"},{"key":"2_CR35","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":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/3-540-45749-6_63","volume-title":"Algorithms - ESA 2002","author":"K. Mehlhorn","year":"2002","unstructured":"Mehlhorn, K., Meyer, U.: External-memory breadth-first search with sublinear I\/O. In: M\u00f6hring, R.H., Raman, R. (eds.) ESA 2002. LNCS, vol.\u00a02461, pp. 723\u2013735. Springer, Heidelberg (2002)"},{"key":"2_CR37","unstructured":"Munagala, K., Ranade, A.: I\/O-complexity of graph algorithms. In: SODA, pp. 687\u2013694 (1999)"},{"key":"2_CR38","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. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 232\u2013249. Springer, Heidelberg (2008)"},{"key":"2_CR39","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)"},{"issue":"2-3","key":"2_CR40","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2-3), 185\u2013204 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"2_CR41","series-title":"GI\/ITG\/GME Workshop","first-page":"81","volume-title":"Methoden des Entwurfs und der Verifikation digitaler Systeme","author":"U. Stern","year":"1996","unstructured":"Stern, U., Dill, D.L.: Combining state space caching and hash compaction. In: Methoden des Entwurfs und der Verifikation digitaler Systeme. GI\/ITG\/GME Workshop, vol.\u00a04, pp. 81\u201390. Shaker Verlag, Aachen (1996)"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Verstoep, K., Bal, H., Barnat, J., Brim, L.: Efficient Large-Scale Model Checking. In: International Symposium on Parallel and Distributed Processing, IPDPS (2009)","DOI":"10.1109\/IPDPS.2009.5161000"},{"issue":"2\/3","key":"2_CR43","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BF01185207","volume":"12","author":"J.S. Vitter","year":"1994","unstructured":"Vitter, J.S., Shriver, E.A.M.: Algorithms for parallel memory; I: two-level memories, II: hierarchical multilevel memories. Algorithmica\u00a012(2\/3), 110\u2013169 (1994)","journal-title":"Algorithmica"},{"key":"2_CR44","unstructured":"Zhou, R., Hansen, E.A.: Structured duplicate detection in external-memory graph search. In: National Conference on Artificial Intelligence (AAAI), pp. 683\u2013689 (2004)"},{"key":"2_CR45","unstructured":"Zhou, R., Hansen, E.A.: Parallel structured duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 1217\u20131222 (2007)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20674-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T04:49:06Z","timestamp":1741150146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20674-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642206733","9783642206740"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20674-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}