{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:00:37Z","timestamp":1725890437883},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851134"},{"type":"electronic","value":"9783540851141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_13","type":"book-chapter","created":{"date-parts":[[2008,8,13]],"date-time":"2008-08-13T03:22:48Z","timestamp":1218597768000},"page":"160-175","source":"Crossref","is-referenced-by-count":6,"title":["Layered Duplicate Detection in External-Memory Model Checking"],"prefix":"10.1007","author":[{"given":"Peter","family":"Lamborn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric A.","family":"Hansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnetic disk instead of main memory in the Mur\u03c6 verifier. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1007\/978-3-540-31980-1_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Bao","year":"2005","unstructured":"Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 526\u2013540. Springer, Heidelberg (2005)"},{"key":"13_CR3","unstructured":"Korf, R., Schultze, P.: Large-scale parallel breadth-first search. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pp. 1380\u20131385 (2005)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: Typical structural properties of state spaces. In: [25], pp. 5\u201322","DOI":"10.1007\/978-3-540-24732-6_2"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-44798-9_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Tronci","year":"2001","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 259\u2013274. Springer, Heidelberg (2001)"},{"key":"13_CR6","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)"},{"issue":"3","key":"13_CR7","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/BF01384077","volume":"7","author":"P. Godefroid","year":"1995","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. Formal Methods in System Design\u00a07(3), 227\u2013241 (1995)","journal-title":"Formal Methods in System Design"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J.: State caching reconsidered. In: [25], pp. 23\u201338","DOI":"10.1007\/978-3-540-24732-6_3"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-36135-9_21","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"L.M. Kristensen","year":"2002","unstructured":"Kristensen, L.M., Mailund, T.: A compositional sweep-line state space exploration method. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 327\u2013343. Springer, Heidelberg (2002)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/3-540-45614-7_31","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L.M. Kristensen","year":"2002","unstructured":"Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 549\u2013567. Springer, Heidelberg (2002)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Parashkevov, A.N., Yantchev, J.: Space efficient reachability analysis through use of pseudo-root states. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 50\u201364 (1997)","DOI":"10.1007\/BFb0035380"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/j.artint.2005.12.002","volume":"170","author":"R. Zhou","year":"2006","unstructured":"Zhou, R., Hansen, E.: Breadth-first heuristic search. Artificial Intelligence\u00a0170, 385\u2013408 (2006)","journal-title":"Artificial Intelligence"},{"key":"13_CR13","unstructured":"Bao, T.: Empirical comparison of algorithms for model checking with magnetic disk. Technical Report VV-0402, Department of Computer Science, Brigham Young University (2004)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11609773_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2005","unstructured":"Jabbar, S., Edelkamp, S.: Parallel external directed model checking with linear I\/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 237\u2013251. Springer, Heidelberg (2005)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-36126-X_13","volume-title":"Formal Methods in Computer-Aided Design","author":"G.D. Penna","year":"2002","unstructured":"Penna, G.D., Intrigila, B., Tronci, E., Zilli, M.V.: Exploiting transition locality in the disk based Mur\u03c6 verifier. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 202\u2013219. Springer, Heidelberg (2002)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-540-39724-3_25","volume-title":"Correct Hardware Design and Verification Methods","author":"G.D. Penna","year":"2003","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Integrating RAM and disk based verification within the Murphi verifier. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 277\u2013282. Springer, Heidelberg (2003)"},{"issue":"4","key":"13_CR17","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G.D. Penna","year":"2004","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Exploiting transition locality in automatic verification of finite-state concurrent systems. International Journal on Software Tools for Technology Transfer\u00a06(4), 320\u2013341 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"13_CR18","unstructured":"Zhou, R., Hansen, E.: Structured duplicate detection in external-memory graph search. In: McGuinness, D.L., Ferguson, G. (eds.) Proceedings of the 19th National Conference on Artificial Intelligence (AAAI 2004), San Jose, CA, pp. 683\u2013688. AAAI Press \/ MIT Press (2004)"},{"key":"13_CR19","volume-title":"11th International Workshop on Formal Methods for Industrial Critical Systems","author":"M. Hammer","year":"2006","unstructured":"Hammer, M., Weber, M.: To Store or not to Store Reloaded: Reclaiming memory on demand. In: 11th International Workshop on Formal Methods for Industrial Critical Systems. Springer, Heidelberg (2006)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The Mur\u03c6 verification system. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"issue":"1","key":"13_CR21","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"13_CR22","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2004.10.016","volume":"128","author":"R. Kumar","year":"2005","unstructured":"Kumar, R., Mercer, E.G.: Load balancing parallel explicit state model checking. Electr. Notes Theor. Comput. Sci.\u00a0128(3), 19\u201334 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Lenoski, D.: DASH Prototype System. PhD thesis, Stanford University (1992)","DOI":"10.1145\/139669.139706"},{"key":"13_CR24","unstructured":"Emerson, A.E., German, S., Havlicek, J., Venkataramani, A.: Model checking a parameterized directory-based cache protocol (2002)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Model Checking Software","year":"2004","unstructured":"Graf, S., Mounier, L. (eds.): SPIN 2004. LNCS, vol.\u00a02989. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:22:07Z","timestamp":1606184527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}