{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T13:55:25Z","timestamp":1774878925991,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434771","type":"print"},{"value":"9783540460176","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_10","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"112-127","source":"Crossref","is-referenced-by-count":19,"title":["Partial Order Reduction in Directed Model Checking"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Lluch-Lafuente","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"Computer Aided Verification (CAV)","author":"R. Alur","year":"1997","unstructured":"R. Alur, R. Brayton, T. Henzinger, S. Qaderer, and S. Rajamani. Partial-order reduction in symbolic state space exploration. In Computer Aided Verification (CAV), Lecture Notes in Computer Science, pages 340\u2013351. Springer, 1997."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"C.-T. Chou and D. Peled. Formal verification of a partial-order reduction technique for model checking. In Tools and Algorithms for Construction and Analysis of Systems, pages 241\u2013257, 1996.","DOI":"10.1007\/3-540-61042-1_48"},{"key":"10_CR3","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil. The right algorithm at the right time: Comparing data flow analysis algorithms for finite state verification. In Proceedings of the 23 rd ICSE, pages 37\u201346, 2001.","DOI":"10.1109\/ICSE.2001.919079"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"D. Dolev, M. Klawe, and M. Rodeh. An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms, 1982.","DOI":"10.1016\/0196-6774(82)90023-2"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"S. Edelkamp, A. L. Lafuente, and S. Leue. Trail-directed model checking. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science, volume 55. Elsevier Science Publishers, 2001.","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"10_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Directed model-checking in HSFSPIN","author":"S. Edelkamp","year":"2001","unstructured":"S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Directed model-checking in HSFSPIN. In 8th International SPIN Workshop on Model Checking Software, Lecture Notes in Computer Science 2057, pages 57\u201379. Springer, 2001."},{"key":"10_CR8","unstructured":"S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI-Spring Symposium on Model-based Validation of Intelligence, pages 75\u201383, 2001."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke, editor, Proceedings of the 2nd International Conference on Computer-Aided Verification (CAV\u2019 90), Rutgers, New Jersey, 1990, number 531, pages 176\u2013185, Berlin-Heidelberg-New York, 1991. Springer.","DOI":"10.1007\/BFb0023731"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"P. E. Hart","year":"1968","unstructured":"P. E. Hart, N. J. Nilsson, and B. Raphael. A formal basis for heuristic determination of minimum path cost. IEEE Transactions on on Systems Science and Cybernetics, 4:100\u2013107, 1968.","journal-title":"IEEE Transactions on on Systems Science and Cybernetics"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"G. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th Int. Conf on Protocol Specification, Testing, and Verification, INWG\/IFIP, Orlando, Fl., June 1992.","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"issue":"2","key":"10_CR12","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1002\/j.1538-7305.1990.tb00101.x","volume":"69","author":"G. J. Holzmann","year":"1990","unstructured":"G. J. Holzmann. Algorithms for automated protocol verification. AT&T Technical Journal, 69(2):32\u201344, Feb. 1990. Special Issue on Protocol Testing, Specification, and Verification.","journal-title":"AT&T Technical Journal"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"M. Kamel and S. Leue. Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. International Journal on Software Tools for Technology Transfer, 2(4):394\u2013409, 2000.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"10_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-46419-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Kamel","year":"2000","unstructured":"M. Kamel and S. Leue. VIP: A visual editor and compiler for v-Promela. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, pages 471\u2013486. Springer, 2000."},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"R. E. Korf. Depth-first iterative-deepening: An optimal admissible tree search. Artificial Intelligence, 27(1):97\u2013109, 1985.","journal-title":"Artificial Intelligence"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigun. Static partial order reduction. In Tools and Algorithms for Construction and Analysis of Systems, pages 345\u2013357, 1998.","DOI":"10.1007\/BFb0054182"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"F. J. Lin, P. M. Chu, and M. Liu. Protocol verification using reachability analysis: the state space explosion problem and relief strategies. ACM, pages 126\u2013135, 1988.","DOI":"10.1145\/55483.55496"},{"issue":"7","key":"10_CR18","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1145\/362619.362631","volume":"14","author":"D. McVitie","year":"1971","unstructured":"D. McVitie and L. Wilson. The stable marriage problem. Communications of the ACM, 14(7):486\u2013492, 1971.","journal-title":"Communications of the ACM"},{"key":"10_CR19","volume-title":"Principles of Artificial Intelligence","author":"N. J. Nilsson","year":"1980","unstructured":"N. J. Nilsson. Principles of Artificial Intelligence. Tioga Publishing Co., Palo Alto, California, 1980."},{"key":"10_CR20","unstructured":"J. Pearl. Heuristics. Addison-Wesley, 1985."},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. A. Peled","year":"1996","unstructured":"D. A. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in Systems Design, 8:39\u201364, 1996.","journal-title":"Formal Methods in Systems Design"},{"key":"10_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D. A. Peled","year":"1998","unstructured":"D. A. Peled. Ten years of partial order reduction. In Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 17\u201328. Springer, 1998."},{"key":"10_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"A stubborn attack on state explosion","author":"A. Valmari","year":"1991","unstructured":"A. Valmari. A stubborn attack on state explosion. Lecture Notes in Computer Science, 531:156\u2013165, 1991."},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"C. H. Yang and D. L. Dill. Validation with guided search of the state space. In Conference on Design Automation (DAC), pages 599\u2013604, 1998.","DOI":"10.1145\/277044.277201"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:45:35Z","timestamp":1558982735000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}