{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T09:30:46Z","timestamp":1775899846465,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_50","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"530-542","source":"Crossref","is-referenced-by-count":20,"title":["Semi-external LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Sanders","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"\u0160ime\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"50_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-68530-8_28","volume-title":"Algorithms - ESA \u201998","author":"J. Abello","year":"1998","unstructured":"Abello, J., Buchsbaum, A.L., Westbrook, J.: A functional approach to external graph algorithms. In: Bilardi, G., Pietracaprina, A., Italiano, G.F., Pucci, G. (eds.) ESA 1998. LNCS, vol.\u00a01461, pp. 332\u2013343. Springer, Heidelberg (1998)"},{"key":"50_CR2","unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Masaryk University Brno, Faculty of Informatics (2004)"},{"key":"50_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11817963_26","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Ro\u010dkai, P., \u0160ime\u010dek, P.: DiVinE \u2013 A Tool for Distributed Verification (Tool Paper). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"key":"50_CR4","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":"50_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/978-3-540-78800-3_5","volume-title":"Proc. of TACAS","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: Proc. of TACAS. LNCS, vol.\u00a04963, pp. 48\u201362. Springer, Heidelberg (2008)"},{"key":"50_CR6","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.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"50_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-73951-7_13","volume-title":"Algorithms and Data Structures","author":"F.C. Botelho","year":"2007","unstructured":"Botelho, F.C., Pagh, R., Ziviani, N.: Simple and space-efficient minimal perfect hash functions. In: Dehne, F.K.H.A., Sack, J.-R., Zeh, N. (eds.) WADS 2007. LNCS, vol.\u00a04619, pp. 139\u2013150. Springer, Heidelberg (2007)"},{"key":"50_CR8","first-page":"653","volume-title":"Conference on Information and Knowledge Management (CIKM)","author":"F.C. Botelho","year":"2007","unstructured":"Botelho, F.C., Ziviani, N.: External perfect hashing for very large key sets. In: Conference on Information and Knowledge Management (CIKM), pp. 653\u2013662. ACM, New York (2007)"},{"key":"50_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, 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":"50_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"50_CR11","unstructured":"Chiang, Y.-J., Goodrich, M.T., Grove, E.F., Tamassia, R., Vengroff, D.E., Vitter, J.S.: External-memory graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 139\u2013149. Society for Industrial and Applied Mathematics (1995)"},{"key":"50_CR12","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"2-3","key":"50_CR13","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des.\u00a01(2-3), 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"50_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"640","DOI":"10.1007\/11561071_57","volume-title":"Proc. of ESA","author":"R. Dementiev","year":"2005","unstructured":"Dementiev, R., Kettner, L., Sanders, P.: STXXL: Standard template library for XXL data sets. In: Proc. of ESA. LNCS, vol.\u00a03669, pp. 640\u2013651. Springer, Heidelberg (2005)"},{"key":"50_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)"},{"issue":"1","key":"50_CR16","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1137\/0605009","volume":"5","author":"M.L. Fredman","year":"1984","unstructured":"Fredman, M.L., Koml\u00f3s, J.: On the size of separating systems and families of perfect hash functions. SIAM Journal on Algebraic and Discrete Methods\u00a05(1), 61\u201368 (1984)","journal-title":"SIAM Journal on Algebraic and Discrete Methods"},{"issue":"2","key":"50_CR17","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1089733.1089735","volume":"37","author":"E. Gal","year":"2005","unstructured":"Gal, E., Toledo, S.: Algorithms and data structures for flash memories. ACM Computing Surveys\u00a037(2), 138\u2013163 (2005)","journal-title":"ACM Computing Surveys"},{"key":"50_CR18","unstructured":"Korf, R.E.: Delayed duplicate detection: Extended abstract. In: International Joint Conference on Artificial Intelligence (IJCAI), pp. 1539\u20131541 (2003)"},{"key":"50_CR19","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":"50_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36574-5","volume-title":"Algorithms for Memory Hierarchies","author":"U. Meyer","year":"2003","unstructured":"Meyer, U.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2003)"},{"key":"50_CR21","unstructured":"Munagala, K., Ranade, A.: I\/O-complexity of graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 687\u2013694. Society for Industrial and Applied Mathematics (1999)"},{"key":"50_CR22","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":"50_CR23","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)"},{"issue":"2\u20133","key":"50_CR24","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. Int. Journal on Software Tools for Technology Transfer\u00a05(2\u20133), 185\u2013204 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"50_CR25","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0898-1221(81)90008-0","volume":"7","author":"M. Sharir","year":"1981","unstructured":"Sharir, M.: A strong-connectivity algorithm and its applications in data flow analysis. Computers and Mathematics with Applications\u00a07(1), 67\u201372 (1981)","journal-title":"Computers and Mathematics with Applications"},{"key":"50_CR26","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 Mur\u03c6 verifier. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 172\u2013183. Springer, Heidelberg (1993)"},{"key":"50_CR27","unstructured":"Zhou, R., Hansen, E.: Breadth-first heuristic search. In: Int. Conf. on Automated Planning and Scheduling (ICAPS) pp. 92\u2013100. AAAI Press \/ The MIT Press (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:22:01Z","timestamp":1620015721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}