{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T09:08:03Z","timestamp":1779354483844,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032267511","type":"print"},{"value":"9783032267528","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-26752-8_8","type":"book-chapter","created":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:14:32Z","timestamp":1779351272000},"page":"126-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Method for\u00a0Testing Partial-Order Reduction Theories in\u00a0Alloy"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-0637-1563","authenticated-orcid":false,"given":"Mara","family":"Miulescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6117-9129","authenticated-orcid":false,"given":"Thomas","family":"Neele","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,22]]},"reference":[{"issue":"10","key":"8_CR1","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1016\/J.SCICO.2010.02.008","volume":"76","author":"N Bene\u0161","year":"2011","unstructured":"Bene\u0161, N., et al.: Partial order reduction for state\/event LTL with application to component-interaction automata. Sci. Comput. Program. 76(10), 877\u2013890 (2011). https:\/\/doi.org\/10.1016\/J.SCICO.2010.02.008","journal-title":"Sci. Comput. Program."},{"key":"8_CR2","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling: entering the SAT competition 2020. In: SAT Competition 2020, pp. 50\u201353 (2020)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"B\u00f8nneland, F.M., Jensen, P.G., Larsen, K.G., Mu\u00f1iz, M., Srba, J.: Partial order reduction for reachability games. In: CONCUR. LIPIcs, vol.\u00a0140, pp. 23:1\u201323:15. Schloss Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2019.23","DOI":"10.4230\/LIPICS.CONCUR.2019.23"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"B\u00f8nneland, F.M., Jensen, P.G., Larsen, K.G., Mu\u00f1iz, M., Srba, J.: Stubborn set reduction for two-player reachability games. Log. Methods Comput. Sci. 17(1) (2021). https:\/\/doi.org\/10.23638\/LMCS-17(1:21)2021","DOI":"10.23638\/LMCS-17(1:21)2021"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-031-33163-3_16","volume-title":"Rigorous State-Based Methods","author":"J Brunel","year":"2023","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: Adding records to alloy. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 212\u2013219. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_16"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/S10817-017-9418-4","volume":"60","author":"J Brunner","year":"2018","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reason. 60(1), 3\u201321 (2018). https:\/\/doi.org\/10.1007\/S10817-017-9418-4","journal-title":"J. Autom. Reason."},{"issue":"3\u20134","key":"8_CR8","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1006225515062","volume":"23","author":"C Chou","year":"1999","unstructured":"Chou, C., Peled, D.A.: Formal verification of a partial-order reduction technique for model checking. J. Autom. Reason. 23(3\u20134), 265\u2013298 (1999). https:\/\/doi.org\/10.1023\/A:1006225515062","journal-title":"J. Autom. Reason."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-319-66107-0_29","volume-title":"Interactive Theorem Proving","author":"M van Delft","year":"2017","unstructured":"van Delft, M., Geuvers, H., Willemse, T.A.C.: A formalisation of consistent consequence for boolean equation systems. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 462\u2013478. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_29"},{"issue":"5","key":"8_CR10","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"RA DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. ACM 22(5), 271\u2013280 (1979). https:\/\/doi.org\/10.1145\/359104.359106","journal-title":"Commun. ACM"},{"issue":"2","key":"8_CR11","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/S10009-010-0137-Y","volume":"12","author":"S Evangelista","year":"2010","unstructured":"Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. Int. J. Softw. Tools Technol. Transf. 12(2), 155\u2013170 (2010). https:\/\/doi.org\/10.1007\/S10009-010-0137-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-540-70545-1_49","volume-title":"Computer Aided Verification","author":"R van Glabbeek","year":"2008","unstructured":"van Glabbeek, R., Ploeger, B.: Correcting a space-efficient simulation algorithm. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 517\u2013529. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_49"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol.\u00a01032. Springer (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7","DOI":"10.1007\/3-540-60761-7"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: The Spin Verification System. DIMACS Series, vol.\u00a032, pp. 23\u201331. DIMACS\/AMS (1996). https:\/\/doi.org\/10.1090\/DIMACS\/032\/03","DOI":"10.1090\/DIMACS\/032\/03"},{"key":"8_CR15","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2012)"},{"issue":"9","key":"8_CR16","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019). https:\/\/doi.org\/10.1145\/3338843","journal-title":"Commun. ACM"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Keiren, J.J.A., Fontana, P., Cleaveland, R.: Corrections to \u201ca menagerie of timed automata\u201d. ACM Comput. Surv. 50(3), 42:1\u201342:8 (2017). https:\/\/doi.org\/10.1145\/3078809","DOI":"10.1145\/3078809"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Laveaux, M., Groote, J.F., Willemse, T.A.C.: Correct and efficient antichain algorithms for refinement checking. Log. Methods Comput. Sci. 17(1) (2021). https:\/\/doi.org\/10.23638\/LMCS-17(1:8)2021","DOI":"10.23638\/LMCS-17(1:8)2021"},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/S10703-016-0267-2","volume":"55","author":"A Milicevic","year":"2019","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. Formal Methods Syst. Des. 55(1), 1\u201332 (2019). https:\/\/doi.org\/10.1007\/S10703-016-0267-2","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR20","unstructured":"Miulescu, M.: Computer-Assisted Verification of Partial-Order Reduction Methods. Master\u2019s thesis, Eindhoven University of Technology (2025)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/978-3-030-45231-5_25","volume-title":"Foundations of Software Science and Computation Structures","author":"T Neele","year":"2020","unstructured":"Neele, T., Valmari, A., Willemse, T.A.C.: The inconsistent labelling problem of stutter-preserving partial-order reduction. In: FoSSaCS 2020. LNCS, vol. 12077, pp. 482\u2013501. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_25"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Neele, T., Valmari, A., Willemse, T.A.C.: A detailed account of the inconsistent labelling problem of stutter-preserving partial-order reduction. Log. Methods Comput. Sci. 17(3) (2021). https:\/\/doi.org\/10.46298\/LMCS-17(3:8)2021","DOI":"10.46298\/LMCS-17(3:8)2021"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-030-45237-7_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Neele","year":"2020","unstructured":"Neele, T., Willemse, T.A.C., Wesselink, W.: Partial-order reduction for parity games with an application on parameterised boolean equation systems. In: TACAS 2020. LNCS, vol. 12079, pp. 307\u2013324. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_19"},{"issue":"5","key":"8_CR24","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/S10009-022-00672-0","volume":"24","author":"T Neele","year":"2022","unstructured":"Neele, T., Willemse, T.A.C., Wesselink, W., Valmari, A.: Partial-order reduction for parity games and parameterised Boolean equation systems. Int. J. Softw. Tools Technol. Transf. 24(5), 735\u2013756 (2022). https:\/\/doi.org\/10.1007\/S10009-022-00672-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR25","unstructured":"Neele, T.S.: Reductions for parity games and model checking. Ph.D. thesis, Technische Universiteit Eindhoven (2020)"},{"issue":"6","key":"8_CR26","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987). https:\/\/doi.org\/10.1137\/0216062","journal-title":"SIAM J. Comput."},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377\u2013390. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_69"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"DA Peled","year":"1996","unstructured":"Peled, D.A.: Combining partial order reductions with on-the-fly model-checking. Formal Methods Syst. Des. 8(1), 39\u201364 (1996). https:\/\/doi.org\/10.1007\/BF00121262","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S1571-0653(04)00311-7","volume":"9","author":"I Shlyakhter","year":"2001","unstructured":"Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Electron. Notes Discret. Math. 9, 19\u201335 (2001). https:\/\/doi.org\/10.1016\/S1571-0653(04)00311-7","journal-title":"Electron. Notes Discret. Math."},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-030-25543-5_27","volume-title":"Computer Aided Verification","author":"SF Siegel","year":"2019","unstructured":"Siegel, S.F.: What\u2019s wrong with on-the-fly partial order reduction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 478\u2013495. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_27"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53863-1_36"},{"issue":"4","key":"8_CR33","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Formal Methods Syst. Des. 1(4), 297\u2013322 (1992). https:\/\/doi.org\/10.1007\/BF00709154","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Valmari, A., Hansen, H.: Stubborn set intuition explained. Trans. Petri Nets Other Model. Concurr. 12, 140\u2013165 (2017)","DOI":"10.1007\/978-3-662-55862-1_7"},{"issue":"1\u20132","key":"8_CR35","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998). https:\/\/doi.org\/10.1016\/S0304-3975(98)00009-7","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26752-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:14:36Z","timestamp":1779351276000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26752-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032267511","9783032267528"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26752-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"22 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2026\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}