{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:38Z","timestamp":1776305318410,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,10,12]],"date-time":"2020-10-12T00:00:00Z","timestamp":1602460800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,10,12]],"date-time":"2020-10-12T00:00:00Z","timestamp":1602460800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,7]]},"DOI":"10.1007\/s10703-020-00350-4","type":"journal-article","created":{"date-parts":[[2020,10,12]],"date-time":"2020-10-12T17:03:24Z","timestamp":1602522204000},"page":"3-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Quasi-optimal partial order reduction"],"prefix":"10.1007","volume":"57","author":[{"given":"Camille","family":"Coti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3154-5268","authenticated-orcid":false,"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"Rodr\u00edguez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Sousa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"key":"350_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla P, Aronis S, Jonsson B, Sagonas K (2014) Optimal dynamic partial order reduction. In: The 41st annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201914). ACM","DOI":"10.1145\/2535838.2535845"},{"key":"350_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Aronis S, Atig MF, Jonsson B, Leonardsson C, Sagonas K (2015) Stateless model checking for TSO and PSO. In: International conference on tools and algorithms for the construction and analysis of systems (TACAS). Springer, pp 353\u2013367","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"350_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Aronis S, Jonsson B, Sagonas K (2017a) Comparing source sets and persistent sets for partial order reduction. In: Models, algorithms, logics and tools\u2014essays dedicated to Kim Guldstrand Larsen on the occasion of his 60th birthday, pp 516\u2013536","DOI":"10.1007\/978-3-319-63121-9_26"},{"issue":"4","key":"350_CR4","doi-asserted-by":"publisher","first-page":"25:1","DOI":"10.1145\/3073408","volume":"64","author":"PA Abdulla","year":"2017","unstructured":"Abdulla PA, Aronis S, Jonsson B, Sagonas K (2017) Source sets: a foundation for optimal dynamic partial order reduction. J ACM 64(4):25:1\u201325:49","journal-title":"J ACM"},{"issue":"OOPSLA","key":"350_CR5","doi-asserted-by":"publisher","first-page":"150:1","DOI":"10.1145\/3360576","volume":"3","author":"PA Abdulla","year":"2019","unstructured":"Abdulla PA, Atig MF, Jonsson B, L\u00e5ng M, Ngo TP (2019) Sagonas K Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc ACM Program Lang 3(OOPSLA):150:1\u2013150:29","journal-title":"Proc ACM Program Lang"},{"key":"350_CR6","doi-asserted-by":"crossref","unstructured":"Albert E, G\u00f3mez-Zamalloa M, Isabel M, Rubio A (2018) Constrained dynamic partial order reduction. In: Chockler H, Weissenbacher G (eds) Computer aided verification\u201430th international conference, CAV 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14\u201317, 2018, Proceedings, Part II, Springer, Lecture Notes in Computer Science, vol 10982, pp 392\u2013410","DOI":"10.1007\/978-3-319-96142-2_24"},{"key":"350_CR7","doi-asserted-by":"publisher","unstructured":"Albert E, de la Banda MG, G\u00f3mez-Zamalloa M, Isabel M, Stuckey PJ (2019) Optimal context-sensitive dynamic partial order reduction with observers. In: Proceedings of the 28th ACM SIGSOFT international symposium on software testing and analysis. Association for Computing Machinery, Beijing, China, ISSTA 2019, pp 352\u2013362. https:\/\/doi.org\/10.1145\/3293882.3330565","DOI":"10.1145\/3293882.3330565"},{"key":"350_CR8","unstructured":"Blktrace (2014) http:\/\/brick.kernel.dk\/snaps\/, version 1.1.0"},{"issue":"POPL","key":"350_CR9","doi-asserted-by":"publisher","first-page":"31:1","DOI":"10.1145\/3158119","volume":"2","author":"M Chalupa","year":"2018","unstructured":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K (2018) Data-centric dynamic partial order reduction. Proc ACM Program Lang 2(POPL):31:1\u201331:30","journal-title":"Proc ACM Program Lang"},{"issue":"OOPSLA","key":"350_CR10","doi-asserted-by":"publisher","first-page":"124:1","DOI":"10.1145\/3360550","volume":"3","author":"K Chatterjee","year":"2019","unstructured":"Chatterjee K, Pavlogiannis A, Toman V (2019) Value-centric dynamic partial order reduction. Proc ACM Program Lang 3(OOPSLA):124:1\u2013124:29","journal-title":"Proc ACM Program Lang"},{"key":"350_CR11","doi-asserted-by":"publisher","unstructured":"Chen D, Jiang Y, Xu C, Ma X, Lu J (2018) Testing multithreaded programs via thread speed control. In: Proceedings of the 2018 26th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering. Association for Computing Machinery, Lake Buena Vista, FL, USA, ESEC\/FSE 2018, pp 15\u201325. https:\/\/doi.org\/10.1145\/3236024.3236077","DOI":"10.1145\/3236024.3236077"},{"key":"350_CR12","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"350_CR13","doi-asserted-by":"crossref","unstructured":"Coons KE, Musuvathi M, McKinley KS (2013) Bounded partial-order reduction. In: OOPSLA, pp 833\u2013848","DOI":"10.1145\/2544173.2509556"},{"key":"350_CR14","doi-asserted-by":"crossref","unstructured":"Esparza J (2010) A false history of true concurrency: From Petri to tools. In: Pol JVD, Weber M (eds) Proceedings of the SPIN, LNCS, vol 6349. Springer, pp 180\u2013186","DOI":"10.1007\/978-3-642-16164-3_13"},{"key":"350_CR15","unstructured":"Esparza J, Heljanko K (2008) Unfoldings\u2014a partial-order approach to model checking. In: EATCS monographs in theoretical computer science. Springer"},{"key":"350_CR16","doi-asserted-by":"crossref","unstructured":"Farzan A, Holzer A, Razavi N, Veith H (2013) Con2colic testing. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering. ACM, New York, NY, USA, ESEC\/FSE 2013, pp 37\u201347","DOI":"10.1145\/2491411.2491453"},{"key":"350_CR17","doi-asserted-by":"publisher","unstructured":"Flanagan C, Godefroid P (2005) Dynamic partial-order reduction for model checking software. In: Principles of programming languages (POPL). ACM, pp 110\u2013121. https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"350_CR18","volume-title":"Partial-order methods for the verification of concurrent systems - An Approach to the State-Explosion Problem, LNCS,","author":"P Godefroid","year":"1996","unstructured":"Godefroid P (1996) Partial-order methods for the verification of concurrent systems - An Approach to the State-Explosion Problem, LNCS, vol 1032. Springer, Berlin"},{"key":"350_CR19","doi-asserted-by":"publisher","unstructured":"Godefroid P (1997) Model checking for programming languages using VeriSoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages. Association for Computing Machinery, Paris, France, POPL \u201997, pp 174\u2013186. https:\/\/doi.org\/10.1145\/263699.263717","DOI":"10.1145\/263699.263717"},{"key":"350_CR20","doi-asserted-by":"crossref","unstructured":"Gueta G, Flanagan C, Yahav E, Sagiv M (2007) Cartesian partial-order reduction. In: Model checking software (SPIN), LNCS, vol 4595. Springer, pp 95\u2013112","DOI":"10.1007\/978-3-540-73370-6_8"},{"key":"350_CR21","unstructured":"MAFFT (2013) http:\/\/mafft.cbrc.jp\/alignment\/software\/, version 7.307"},{"key":"350_CR22","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz A (1987) Trace theory. In: Petri nets: applications and relationships to other models of concurrency, LNCS, vol 255. Springer, pp 278\u2013324","DOI":"10.1007\/3-540-17906-2_30"},{"key":"350_CR23","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Bochmann GV, Probst DK (eds) Proceedings of the CAV\u201992, LNCS, vol 663. Springer, pp 164\u2013177","DOI":"10.1007\/3-540-56496-9_14"},{"issue":"4","key":"350_CR24","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541\u2013580","journal-title":"Proc IEEE"},{"key":"350_CR25","doi-asserted-by":"publisher","unstructured":"Musuvathi M, Qadeer S (2007) Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the 28th ACM SIGPLAN conference on programming language design and implementation, PLDI \u201907. Association for Computing Machinery, San Diego, California, USA, pp 446\u2013455. https:\/\/doi.org\/10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785"},{"key":"350_CR26","doi-asserted-by":"publisher","unstructured":"Nguyen HTT, Rodr\u00edguez C, Sousa M, Coti C, Petrucci L (2018) Quasi-optimal partial order reduction. In: Chockler H, Weissenbacher G (eds) Computer aided verification, lecture notes in computer science. Springer International Publishing, pp 354\u2013371. https:\/\/doi.org\/10.1007\/978-3-319-96142-2_22","DOI":"10.1007\/978-3-319-96142-2_22"},{"key":"350_CR27","doi-asserted-by":"crossref","unstructured":"Nielsen M, Plotkin GD, Winskel G (1979) Petri nets, event structures and domains. In: Proceedings of the international symposium on semantics of concurrent computation. LNCS, vol 70. Springer, pp 266\u2013284","DOI":"10.1007\/BFb0022474"},{"issue":"1","key":"350_CR28","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M Nielsen","year":"1981","unstructured":"Nielsen M, Plotkin G, Winskel G (1981) Petri nets, event structures and domains, part I. Theor Comput Sci 13(1):85\u2013108","journal-title":"Theor Comput Sci"},{"key":"350_CR29","doi-asserted-by":"publisher","unstructured":"Pham TA, J\u00e9ron T, Quinson M (2019) Unfolding-based dynamic partial order reduction of asynchronous distributed programs. In: P\u00e9rez JA, Yoshida N (eds) Formal techniques for distributed objects, components, and systems\u201439th IFIP WG 6.1 international conference, FORTE 2019, held as part of the 14th international federated conference on distributed computing techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17\u201321, 2019, Proceedings, Springer, Lecture Notes in Computer Science, vol 11535, pp 224\u2013241. https:\/\/doi.org\/10.1007\/978-3-030-21759-4_13","DOI":"10.1007\/978-3-030-21759-4_13"},{"key":"350_CR30","doi-asserted-by":"crossref","unstructured":"Pugh W (1989) Skip lists: a probabilistic alternative to balanced trees. In: Algorithms and data structures, workshop WADS \u201989, Ottawa, Canada, August 17\u201319, 1989, Proceedings, pp 437\u2013449","DOI":"10.1007\/3-540-51542-9_36"},{"key":"350_CR31","unstructured":"Rodr\u00edguez C, Sousa M, Sharma S, Kroening D (2015a) Unfolding-based partial order reduction. In: Proceedings of the CONCUR, pp 456\u2013469"},{"key":"350_CR32","unstructured":"Rodr\u00edguez C, Sousa M, Sharma S, Kroening D (2015b) Unfolding-based partial order reduction. CoRR arXiv:1507.00980"},{"key":"350_CR33","doi-asserted-by":"publisher","unstructured":"Schemmel D, B\u00fcning J, Rodr\u00edguez C, Laprell D, Wehrle K (2020) Symbolic partial-order execution for testing multi-threaded programs. In: Lahiri SK, Wang C (eds) Computer aided verification, lecture notes in computer science. Springer International Publishing, Cham, pp 376\u2013400. https:\/\/doi.org\/10.1007\/978-3-030-53288-8_18","DOI":"10.1007\/978-3-030-53288-8_18"},{"key":"350_CR34","doi-asserted-by":"crossref","unstructured":"Sousa M, Rodr\u00edguez C, D\u2019Silva V, Kroening D (2017) Abstract interpretation with unfoldings. CoRR arXiv:1705.00595","DOI":"10.1007\/978-3-319-63390-9_11"},{"issue":"4","key":"350_CR35","doi-asserted-by":"publisher","first-page":"23:1","DOI":"10.1145\/2858651","volume":"2","author":"P Thomson","year":"2016","unstructured":"Thomson P, Donaldson AF, Betts A (2016) Concurrency testing using controlled schedulers: an empirical study. TOPC 2(4):23:1\u201323:37","journal-title":"TOPC"},{"key":"350_CR36","doi-asserted-by":"crossref","unstructured":"Wang C, Yang Z, Kahlon V, Gupta A (2008) Peephole partial order reduction. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems, 14th international conference, TACAS 2008, held as part of the joint european conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol 4963. Springer, pp 382\u2013396","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"350_CR37","doi-asserted-by":"crossref","unstructured":"Yang Y, Chen X, Gopalakrishnan G, Kirby RM (2008) Efficient stateful dynamic partial order reduction. In: Model checking software (SPIN), LNCS, vol 5156. Springer, pp 288\u2013305","DOI":"10.1007\/978-3-540-85114-1_20"},{"key":"350_CR38","doi-asserted-by":"crossref","unstructured":"Yu J, Narayanasamy S, Pereira C, Pokam G (2012) Maple: a coverage-driven testing tool for multithreaded programs. In: OOPSLA, pp 485\u2013502","DOI":"10.1145\/2398857.2384651"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00350-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00350-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00350-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,12]],"date-time":"2021-10-12T10:50:12Z","timestamp":1634035812000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00350-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,12]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,7]]}},"alternative-id":["350"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00350-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,12]]},"assertion":[{"value":"26 June 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 September 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 October 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}