{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:51:46Z","timestamp":1773193906294,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11407-N23"],"award-info":[{"award-number":["S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-003"],"award-info":[{"award-number":["ICT15-003"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>\n            The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the\n            <jats:italic>happens-before<\/jats:italic>\n            equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i)\u00a0the size of the partitioning induced by the equivalence, and (ii)\u00a0the time spent by the exploration algorithm in each class of the partitioning.\n          <\/jats:p>\n          <jats:p>\n            In this work, we present a new equivalence, called\n            <jats:italic>value-happens-before<\/jats:italic>\n            and show that it has two appealing features. First, value-happens-before is always at least\n            <jats:italic>as coarse as<\/jats:italic>\n            the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called\n            <jats:italic>value-centric<\/jats:italic>\n            DPOR (\n            <jats:italic>VCDPOR<\/jats:italic>\n            ), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of\n            <jats:italic>VCDPOR<\/jats:italic>\n            on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.\n          <\/jats:p>","DOI":"10.1145\/3360550","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Value-centric dynamic partial order reduction"],"prefix":"10.1145","volume":"3","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Toman","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Parosh Abdulla Stavros Aronis Bengt Jonsson and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction (POPL).  Parosh Abdulla Stavros Aronis Bengt Jonsson and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction (POPL).","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_2_1","volume-title":"Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas.","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla , Stavros Aronis , Mohamed Faouzi Atig , Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015 . Stateless Model Checking for TSO and PSO. In TACAS. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In TACAS."},{"key":"e_1_2_1_3_1","volume-title":"Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey.","author":"Albert Elvira","year":"2017","unstructured":"Elvira Albert , Puri Arenas , Mar\u00eda Garc\u00eda de la Banda , Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey. 2017 . Context-Sensitive Dynamic Partial Order Reduction. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham, 526\u2013543. Elvira Albert, Puri Arenas, Mar\u00eda Garc\u00eda de la Banda, Miguel G\u00f3mez-Zamalloa, and Peter J. Stuckey. 2017. Context-Sensitive Dynamic Partial Order Reduction. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham, 526\u2013543."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Jade Alglave Daniel Kroening and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV.  Jade Alglave Daniel Kroening and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV.","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_2_1_5_1","volume-title":"Zing: A Model Checker for Concurrent Software. In CAV.","author":"Andrews Tony","year":"2004","unstructured":"Tony Andrews , Shaz Qadeer , Sriram K. Rajamani , Jakob Rehof , and Yichen Xie . 2004 . Zing: A Model Checker for Concurrent Software. In CAV. Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, and Yichen Xie. 2004. Zing: A Model Checker for Concurrent Software. In CAV."},{"key":"e_1_2_1_6_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Aronis Stavros","unstructured":"Stavros Aronis , Bengt Jonsson , Magnus L\u00e5ng , and Konstantinos Sagonas . 2018. Optimal Dynamic Partial Order Reduction with Observers . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing , Cham , 229\u2013248. Stavros Aronis, Bengt Jonsson, Magnus L\u00e5ng, and Konstantinos Sagonas. 2018. Optimal Dynamic Partial Order Reduction with Observers. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 229\u2013248."},{"key":"e_1_2_1_7_1","volume-title":"In Proceedings of the 18th Annual Allerton Conference on Communication, Control, and Computing. Citeseer.","author":"Burns James","year":"1980","unstructured":"James Burns and Nancy A Lynch . 1980 . Mutual exclusion using invisible reads and writes . In In Proceedings of the 18th Annual Allerton Conference on Communication, Control, and Computing. Citeseer. James Burns and Nancy A Lynch. 1980. Mutual exclusion using invisible reads and writes. In In Proceedings of the 18th Annual Allerton Conference on Communication, Control, and Computing. Citeseer."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Jean-Marie Cadiou and Jean-Jacques L\u00e9vy. 1973. Mechanizable proofs about parallel processes. In SWAT.  Jean-Marie Cadiou and Jean-Jacques L\u00e9vy. 1973. Mechanizable proofs about parallel processes. In SWAT.","DOI":"10.1109\/SWAT.1973.14"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Andreas Pavlogiannis and Viktor Toman. 2019. Value-centric Dynamic Partial Order Reduction. arXiv: arXiv:1909.00989  Krishnendu Chatterjee Andreas Pavlogiannis and Viktor Toman. 2019. Value-centric Dynamic Partial Order Reduction. arXiv: arXiv:1909.00989","DOI":"10.1145\/3360550"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_13_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Jr., Orna Grumberg , and Doron A . Peled . 1999 a. Model Checking. MIT Press , Cambridge, MA, USA. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999a. Model Checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_1_14_1","volume-title":"2-thread software solutions for the mutual exclusion problem. https: \/\/github.com\/pramalhe\/ConcurrencyFreaks\/blob\/master\/papers\/cr2t-","author":"Correia Andreia","year":"2016","unstructured":"Andreia Correia and Pedro Ramalhete . 2016. 2-thread software solutions for the mutual exclusion problem. https: \/\/github.com\/pramalhe\/ConcurrencyFreaks\/blob\/master\/papers\/cr2t- 2016 .pdf . Andreia Correia and Pedro Ramalhete. 2016. 2-thread software solutions for the mutual exclusion problem. https: \/\/github.com\/pramalhe\/ConcurrencyFreaks\/blob\/master\/papers\/cr2t- 2016.pdf ."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/357980.357989"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan and Zachary Kincaid. 2012. Verification of parameterized concurrent programs by modular reasoning about data and control. In CAV.  Azadeh Farzan and Zachary Kincaid. 2012. Verification of parameterized concurrent programs by modular reasoning about data and control. In CAV.","DOI":"10.1145\/2103656.2103693"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Azadeh Farzan and P. Madhusudan. 2009. The Complexity of Predicting Atomicity Violations. In TACAS.  Azadeh Farzan and P. Madhusudan. 2009. The Complexity of Predicting Atomicity Violations. In TACAS.","DOI":"10.1007\/978-3-642-00768-2_14"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.  Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_20_1","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"Godefroid P.","unstructured":"P. Godefroid . 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem . Springer-Verlag , Secaucus, NJ, USA . P. Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, Secaucus, NJ, USA."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid. 1997. Model Checking for Programming Languages Using VeriSoft. In POPL.  Patrice Godefroid. 1997. Model Checking for Programming Languages Using VeriSoft. In POPL.","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384077"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In PLDI.  Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In PLDI.","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984025"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.16"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Kari K\u00e4hk\u00f6nen Olli Saarikivi and Keijo Heljanko. 2012. Using Unfoldings in Automated Testing of Multithreaded Programs. In ACSD.  Kari K\u00e4hk\u00f6nen Olli Saarikivi and Keijo Heljanko. 2012. Using Unfoldings in Automated Testing of Multithreaded Programs. In ACSD.","DOI":"10.1145\/2351676.2351698"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90054-J"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288966"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/355592.365595"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Steven Lauterburg Rajesh K. Karmani Darko Marinov and Gul Agha. 2010. Evaluating Ordering Heuristics for Dynamic Partial-order Reduction Techniques. In FASE.  Steven Lauterburg Rajesh K. Karmani Darko Marinov and Gul Agha. 2010. Evaluating Ordering Heuristics for Dynamic Partial-order Reduction Techniques. In FASE.","DOI":"10.1007\/978-3-642-12029-9_22"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_35_1","volume-title":"CHESS: A systematic testing tool for concurrent software. Technical Report.","author":"Madan Musuvathi Tom Ball","year":"2007","unstructured":"Tom Ball Madan Musuvathi , Shaz Qadeer . 2007 . CHESS: A systematic testing tool for concurrent software. Technical Report. Tom Ball Madan Musuvathi, Shaz Qadeer. 2007. CHESS: A systematic testing tool for concurrent software. Technical Report."},{"key":"e_1_2_1_36_1","volume-title":"Advances in Petri Nets","author":"Mazurkiewicz A","year":"1986","unstructured":"A Mazurkiewicz . 1987. Trace Theory . In Advances in Petri Nets 1986 , Part II on Petri Nets : Applications and Relationships to Other Models of Concurrency. Springer-Verlag New York , Inc., 279\u2013324. A Mazurkiewicz. 1987. Trace Theory. In Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency. Springer-Verlag New York, Inc., 279\u2013324."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250785"},{"key":"e_1_2_1_39_1","volume-title":"Piramanayagam Arumuga Nainar, and Iulian Neamtiu","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , Gerard Basler , Piramanayagam Arumuga Nainar, and Iulian Neamtiu . 2008 . Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_22"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Doron Peled. 1993. All from One One for All: On Model Checking Using Representatives. In CAV.  Doron Peled. 1993. All from One One for All: On Model Checking Using Representatives. In CAV.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803398"},{"key":"e_1_2_1_45_1","unstructured":"C\u00e9sar Rodr\u00edguez Marcelo Sousa Subodh Sharma and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR.  C\u00e9sar Rodr\u00edguez Marcelo Sousa Subodh Sharma and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR."},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Olli Saarikivi Kari Kahkonen and Keijo Heljanko. 2012. Improving Dynamic Partial Order Reductions for Concolic Testing. In ACSD.  Olli Saarikivi Kari Kahkonen and Keijo Heljanko. 2012. Improving Dynamic Partial Order Reductions for Concolic Testing. In ACSD.","DOI":"10.1109\/ACSD.2012.18"},{"key":"e_1_2_1_47_1","unstructured":"Koushik Sen and Gul Agha. 2006. Automated Systematic Testing of Open Distributed Programs. In FASE.  Koushik Sen and Gul Agha. 2006. Automated Systematic Testing of Open Distributed Programs. In FASE."},{"key":"e_1_2_1_48_1","unstructured":"Koushik Sen and Gul Agha. 2007. A Race-detection and Flipping Algorithm for Automated Testing of Multi-threaded Programs. In HVC.  Koushik Sen and Gul Agha. 2007. A Race-detection and Flipping Algorithm for Automated Testing of Multi-threaded Programs. In HVC."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/55364.55425"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Samira Tasharofi Rajesh K. Karmani Steven Lauterburg Axel Legay Darko Marinov and Gul Agha. 2012. TransDPOR: A Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In FMOODS\/FORTE.  Samira Tasharofi Rajesh K. Karmani Steven Lauterburg Axel Legay Darko Marinov and Gul Agha. 2012. TransDPOR: A Novel Dynamic Partial-order Reduction Technique for Testing Actor Programs. In FMOODS\/FORTE.","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/645955.675799"},{"key":"e_1_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Antti Valmari. 1991. Stubborn Sets for Reduced State Space Generation. In Petri Nets.  Antti Valmari. 1991. Stubborn Sets for Reduced State Space Generation. In Petri Nets.","DOI":"10.1007\/3-540-53863-1_36"},{"key":"e_1_2_1_53_1","unstructured":"Chao Wang Zijiang Yang Vineet Kahlon and Aarti Gupta. 2008. Peephole Partial Order Reduction. In TACAS.  Chao Wang Zijiang Yang Vineet Kahlon and Aarti Gupta. 2008. Peephole Partial Order Reduction. In TACAS."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360550","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360550","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360550"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":52,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360550"],"URL":"https:\/\/doi.org\/10.1145\/3360550","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}