{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:40Z","timestamp":1760202520981,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028760","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"379-390","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["A general approach to partial order reductions in symbolic verification"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"given":"Mats","family":"Kindahl","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"35_CR1","first-page":"340","volume-title":"Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254","author":"R. Alur","year":"1997","unstructured":"R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani. Partial-order reduction in symbolic state space exploration. In O. Grumberg, editor, Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254, pages 340\u2013351, Haifa, Israel, 1997. Springer Verlag."},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 414-425, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"35_CR3","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Karlis \u010cer\u0101ns, Bengt Jonsson, and Tsay Yih-Kuen. General decidability theorems for infinite-state systems. In Proc. 11 th IEEE Int. Symp. on Logic in Computer Science, pages 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8 th IEEE Int. Symp. on Logic in Computer Science, pages 160\u2013170, 1993.","DOI":"10.1109\/LICS.1993.287591"},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla, Mats Kindahl, and Doron Peled. An improved search strategy for Lossy Channel Systems. In Tadanori Mizuno, Nori Shiratori, Teruo Hegashino, and Atsushi Togashi, editors, FORTE X \/ PST V XVII '97, pages 251\u2013264. Chapman and Hall, 1997.","DOI":"10.1007\/978-0-387-35271-8_16"},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"R.J.R. Back. A method for refining atomicity in parallel algorithms. In Proc. PARLE 89, volume 366 of Lecture Notes in Computer Science, pages 199\u2013216. Springer Verlag, 1989.","DOI":"10.1007\/3-540-51285-3_42"},{"key":"35_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 102o states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Alur and Henzinger, editors, Proc. 8 th Int. Conf. on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 1\u201312. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"key":"35_CR9","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A. Finkel","year":"1990","unstructured":"A. Finkel. Reduction and covering of infinite reachability trees. Information and Computation, 89:144\u2013179, 1990.","journal-title":"Information and Computation"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Proc. 5th Conference on Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid, D. Pirottin. Refining Dependencies Improves Partial-Order Verification Methods. Proc. 5th Conference on Computer Aided Verification, Lecture Notes in Computer Science 697, Springer, 438\u2013449. Elounda, Greece, 1993."},{"key":"35_CR11","unstructured":"P. Godefroid and P. Wolper. Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. In Formal Methods in System Design, Kluwer, 2 (1993), 149\u2013164."},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and D. Peled. An improvement in formal verification. In Proc. FORTE '94, pages 197\u2013211, 1994.","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"[JZ92] W. Janssen and J. Zwiers. From sequential layers to distributed processes. In Proc. 11 th ACM Symp. on Principles of Distributed Computing, Canada, 1992.","DOI":"10.1145\/135419.135461"},{"key":"35_CR14","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"Shmuel Katz and Doron Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337\u2013359, 1992.","journal-title":"Theoretical Computer Science"},{"key":"35_CR15","unstructured":"R.P. Kurshan, V. Levin, M. Minea and D. Peled, H. Yenigun,. Static Partial Order Reduction. TACAS'98, Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal."},{"issue":"2","key":"35_CR16","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BF01786631","volume":"4","author":"L. Lamport","year":"1990","unstructured":"L. Lamport. A theorem on atomicity in distributed algorithms. Distributed Computing, 4(2):59\u201368, 1990.","journal-title":"Distributed Computing"},{"issue":"12","key":"35_CR17","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"Lipton","year":"1975","unstructured":"Lipton. Reduction, a method of proving properties of parallel programs. Communications of the ACM, 18(12):717\u2013721, Dec. 1975.","journal-title":"Communications of the ACM"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In Proc. 18 th IEEE Real-Time Systems Symposium, pages 14\u201324, San Francisco, California, Dec. 1997.","DOI":"10.1109\/REAL.1997.641265"},{"issue":"1","key":"35_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"K.L. McMillan","year":"1995","unstructured":"K.L. McMillan. A technique of a state space search based on unfolding. Formal Methods in System Design, 6(1):45\u201365, 1995.","journal-title":"Formal Methods in System Design"},{"key":"35_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"D. Peled","year":"1996","unstructured":"D. Peled. Combining Partial Order Reductions with On-the-fly Model-Checking. Journal of Formal Methods in Systems Design, 8 (1996), 39\u201364.","journal-title":"Journal of Formal Methods in Systems Design"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"A. Valmari. Stubborn sets for reduced state space generation. In Advances in Petri Nets, number 483 in Lecture Notes in Computer Science, pages 491\u2013515. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-53863-1_36"},{"key":"35_CR22","doi-asserted-by":"crossref","unstructured":"A. Valmari. On-the-fly verification with stubborn sets. In Courcoubetis, editor, Proc. 5 th Int. Conf. on Computer Aided Verification, number 697 in Lecture Notes in Computer Science, pages 59\u201370, 1993.","DOI":"10.1007\/3-540-56922-7_33"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028760","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T01:44:25Z","timestamp":1736127865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028760"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0028760","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}