{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:11Z","timestamp":1725551951616},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_16","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"237-251","source":"Crossref","is-referenced-by-count":19,"title":["Parallel External Directed Model Checking with Linear I\/O"],"prefix":"10.1007","author":[{"given":"Shahid","family":"Jabbar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 disks. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 526\u2013540. Springer, Heidelberg (2005)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-40922-X_24","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Ben-David","year":"2000","unstructured":"Ben-David, S., Heyman, T., Grumberg, O., Schuster, A.: Scalable distributed on-the-fly symbolic model checking. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 390\u2013404. Springer, Heidelberg (2000)"},{"key":"16_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification","author":"B. B\u00e9rard","year":"2001","unstructured":"B\u00e9rard, B., Bidoit, A.F.M., Laroussine, F., Petit, A., Petrucci, L., Schoenebelen, P., McKenzie, P.: Systems and Software Verification. Springer, Heidelberg (2001)"},{"key":"16_CR4","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":"L. Brim","year":"2001","unstructured":"Brim, L., Barnat, J., Stribnra, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"16_CR5","unstructured":"Edelkamp, S.: External symbolic pattern databases. In: International Conference on Automated Planning and Scheduling (ICAPS), pp. 51\u201360 (2005)"},{"key":"16_CR6","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)"},{"issue":"2\u20133","key":"16_CR7","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology\u00a05(2\u20133), 247\u2013267 (2004)","journal-title":"International Journal on Software Tools for Technology"},{"key":"16_CR8","unstructured":"Edelkamp, S., Schr\u00f6dl, S.: Localizing A*. In: National Conference on Artificial Intelligence (AAAI), pp. 885\u2013890 (2000)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Heuristic model checking for java programs. International Journal on Software Tools for Technology Transfer\u00a06(4) (2004)","DOI":"10.1007\/s10009-003-0130-9"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Computer Aided Verification","author":"T. Heyman","year":"2000","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 20\u201335. Springer, Heidelberg (2000)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-30579-8_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2005","unstructured":"Jabbar, S., Edelkamp, S.: I\/O efficient directed model checking. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 313\u2013329. Springer, Heidelberg (2005)"},{"issue":"4","key":"16_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"Kamel, M., Leue, S.: Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. International Journal on Software Tools for Technology Transfer\u00a02(4), 394\u2013409 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR13","unstructured":"Korf, R.: Best-first frontier search with delayed duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 650\u2013657 (2004)"},{"key":"16_CR14","unstructured":"Korf, R.E., Schultze, P.: Large-scale parallel breadth-first search. In: National Conference on Artificial Intelligence (AAAI), pp. 1380\u20131385 (2005)"},{"key":"16_CR15","unstructured":"Korf, R.E., Zhang, W.: Divide-and-conquer frontier search applied to optimal sequence allignment. In: National Conference on Artificial Intelligence (AAAI), pp. 910\u2013916 (2000)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-39893-6_19","volume-title":"Formal Methods and Software Engineering","author":"L.M. Kristensen","year":"2003","unstructured":"Kristensen, L.M., Mailund, T.: Path finding with the sweep-line method using external storage. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 319\u2013337. Springer, Heidelberg (2003)"},{"key":"16_CR17","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-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 22. Springer, Heidelberg (1999)"},{"key":"16_CR18","unstructured":"Lluch-Lafuente, A.: Directed Search for the Verification of Communication Protocols. PhD thesis, University of Freiburg (2003)"},{"key":"16_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, Dordrecht (1993)"},{"key":"16_CR20","first-page":"117","volume-title":"Verification of Digital and Hybrid Systems","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Symmetry and model checking. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems, pp. 117\u2013137. Springer, Heidelberg (1998)"},{"key":"16_CR21","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":"16_CR22","unstructured":"Munagala, K., Ranade, A.: I\/O-complexity of graph algorithms. In: Symposium on Discrete Algorithms (SODA), pp. 87\u201388 (2001)"},{"key":"16_CR23","volume-title":"Heuristics","author":"J. Pearl","year":"1985","unstructured":"Pearl, J.: Heuristics. Addison-Wesley, Reading (1985)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D.A. Peled","year":"1998","unstructured":"Peled, D.A.: Ten years of partial order reduction. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 17\u201328. Springer, Heidelberg (1998)"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J.H. Reif","year":"1985","unstructured":"Reif, J.H.: Depth-first search is inherently sequential. Information Processing Letters\u00a020, 229\u2013234 (1985)","journal-title":"Information Processing Letters"},{"key":"16_CR26","volume-title":"Algorithms for Memory Hierarchies","author":"P. Sanders","year":"2002","unstructured":"Sanders, P., Meyer, U., Sibeyn, J.F.: Algorithms for Memory Hierarchies. Springer, Heidelberg (2002)"},{"key":"16_CR27","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.: Using magnetic disk instead of main memory in the murphi verifier. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.L.: Parallelizing the Murphi verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Conference on Design Automation (DAC), pp. 599\u2013604 (1998)","DOI":"10.1145\/277044.277201"},{"key":"16_CR30","unstructured":"Zhou, R., Hansen, E.: Structured duplicate detection in external-memory graph search. In: National Conference on Artificial Intelligence (AAAI), pp. 683\u2013689 (2004)"},{"key":"16_CR31","unstructured":"Zhou, R., Hansen, E.: External-memory pattern databases using delayed duplicate detection. In: National Conference on Artificial Intelligence (AAAI), pp. 1398\u20131405 (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:06:59Z","timestamp":1619507219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11609773_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}