{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:42:39Z","timestamp":1779392559806,"version":"3.53.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_14","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"188-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Practical Partial Order Reduction for CSP"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Gibson-Robinson","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Henri","family":"Hansen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xu","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"14_CR2","unstructured":"Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Roscoe, A.: Understanding Concurrent Systems (2010)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 A modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)"},{"key":"14_CR5","unstructured":"University of Oxford, Failures-Divergence Refinement\u2013FDR 3 User Manual (2014). https:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991)"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification (CAV)","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) Computer Aided Verification (CAV). LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: Application of Concurrency to System Design (ACSD) (2011)","DOI":"10.1109\/ACSD.2011.25"},{"key":"14_CR10","unstructured":"Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification (1997)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1007\/978-3-540-45236-2_33","volume-title":"FME 2003: Formal Methods","author":"M Goldsmith","year":"2003","unstructured":"Goldsmith, M., Moffat, N., Roscoe, A.W., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model-checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 600\u2013616. Springer, Heidelberg (2003)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Valmari, A., Hansen, H.: Can stubborn sets be optimal?. Fundamenta Informaticae 113(3) (2011)","DOI":"10.3233\/FI-2011-613"},{"key":"14_CR13","unstructured":"Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. PhD thesis, Helsinki University of Technology (1998)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/978-3-642-39176-7_15","volume-title":"Model Checking Software","author":"A Laarman","year":"2013","unstructured":"Laarman, A., Pater, E., van de Pol, J., Weber, M.: Guard-based partial-order reduction. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 227\u2013245. Springer, Heidelberg (2013)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. International Journal on Software Tools for Technology Transfer 12(2) (2010)","DOI":"10.1007\/s10009-010-0137-y"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-55179-4_32","volume-title":"Computer Aided Verification","author":"P Godefroid","year":"1992","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 332\u2013342. Springer, Heidelberg (1992)"},{"key":"14_CR17","unstructured":"Varpaaniemi, K.: Minimizing the number of successor states in the stubborn set method. Fundamenta Informaticae 51(1) (2002)"},{"key":"14_CR18","unstructured":"Valmari, A.: State space generation: Efficiency and practicality. PhD thesis, Tampere University of Technology (1988)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AW Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D., Scattergood, J.: Hierarchical compression for model-checking CSP or how to check 10$$^{20}$$ dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/978-3-319-11737-9_2","volume-title":"Formal Methods and Software Engineering","author":"A Boulgakov","year":"2014","unstructured":"Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal bisimulations. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 11\u201326. Springer, Heidelberg (2014)"},{"key":"14_CR21","unstructured":"Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. In: AVoCS (2007)"},{"key":"14_CR22","unstructured":"Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In Communicating Process Architectures (2014)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T12:41:30Z","timestamp":1676637690000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}