{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:39Z","timestamp":1776305319658,"version":"3.50.1"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stateless model checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are <jats:italic>optimal<\/jats:italic> are particularly effective in that they guarantee to explore <jats:italic>exactly<\/jats:italic> one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in <jats:sc>Nidhugg<\/jats:sc> shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to TruSt, a related optimal DPOR algorithm that represents executions as graphs, shows that POP \u2019s implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt \u2019s on programs with long executions.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_2","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"19-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Parsimonious Optimal Dynamic Partial Order Reduction"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7029-1904","authenticated-orcid":false,"given":"Sarbojit","family":"Das","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7897-601X","authenticated-orcid":false,"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9657-0179","authenticated-orcid":false,"given":"Konstantinos","family":"Sagonas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Symposium on Principles of Programming Languages, pp. 373\u2013384. POPL 2014, ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","DOI":"10.1145\/2535838.2535845"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1\u201325:49 (2017). https:\/\/doi.org\/10.1145\/3073408","DOI":"10.1145\/3073408"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., B\u00f8nneland, F.M., Das, S., Jonsson, B., L\u00e5ng, M., Sagonas, K.: Tailoring stateless model checking for event-driven multi-threaded programs. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings, Part II. LNCS, vol. 14216, pp. 176\u2013198. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_9","DOI":"10.1007\/978-3-031-45332-8_9"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Das, S., Jonsson, B., Sagonas, K.: Parsimonious optimal dynamic partial order reduction (2024). https:\/\/doi.org\/10.48550\/arXiv.2405.11128, https:\/\/doi.org\/10.48550\/arXiv.2405.11128, Extended Version with Proofs","DOI":"10.48550\/arXiv.2405.11128"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ng, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3(OOPSLA), 150:1\u2013150:29 (2019). https:\/\/doi.org\/10.1145\/3360576","DOI":"10.1145\/3360576"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-41540-6_8","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. Proc. ACM on Program. Lang. 2(OOPSLA), 135:1\u2013135:29 (2018). https:\/\/doi.org\/10.1145\/3276505","DOI":"10.1145\/3276505"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Albert, E., de\u00a0la Banda, M.G., G\u00f3mez-Zamalloa, M., Isabel, M., Stuckey, P.J.: Optimal dynamic partial order reduction with context-sensitive independence and observers. J. Syst. Softw. 202, 111730 (2023). https:\/\/doi.org\/10.1016\/J.JSS.2023.111730","DOI":"10.1016\/J.JSS.2023.111730"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-319-96142-2_24","volume-title":"Computer Aided Verification","author":"E Albert","year":"2018","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Isabel, M., Rubio, A.: Constrained dynamic partial order reduction. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 392\u2013410. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_24"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-319-89963-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Aronis","year":"2018","unstructured":"Aronis, S., Jonsson, B., L\u00e5ng, M., Sagonas, K.: Optimal dynamic partial order reduction with observers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 229\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_14"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, pp. 167\u2013178. ASPLOS XV, ACM, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1736020.1736040","DOI":"10.1145\/1736020.1736040"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., Vaidya, K.: Data-centric dynamic partial order reduction. Proc. ACM on Program. Lang. 2(POPL), 31:1\u201331:30 (2018). https:\/\/doi.org\/10.1145\/3158119","DOI":"10.1145\/3158119"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Pavlogiannis, A., Toman, V.: Value-centric dynamic partial order reduction. Proc. ACM Program. Lang. 3(OOPSLA), 124:1\u2013124:29 (2019). https:\/\/doi.org\/10.1145\/3360550","DOI":"10.1145\/3360550"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, pp. 154\u2013163. ICST 2013, IEEE, Los Alamitos, CA, USA (2013). https:\/\/doi.org\/10.1109\/ICST.2013.50","DOI":"10.1109\/ICST.2013.50"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Demsky, B., Lam, P.: SATCheck: SAT-directed stateless model checking for SC and TSO. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 20\u201336. OOPSLA 2015, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2814270.2814297","DOI":"10.1145\/2814270.2814297"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 411\u2013422. POPL 2011, ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926432","DOI":"10.1145\/1926385.1926432"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of Programming Languages, (POPL), pp. 110\u2013121. ACM, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","DOI":"10.1145\/1040305.1040315"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: Principles of Programming Languages, (POPL), pp. 174\u2013186. ACM Press, New York, NY, USA (1997). https:\/\/doi.org\/10.1145\/263699.263717","DOI":"10.1145\/263699.263717"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005). https:\/\/doi.org\/10.1007\/s10703-005-1489-x","DOI":"10.1007\/s10703-005-1489-x"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Hanmer, R.S., Jagadeesan, L.: Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 124\u2013133. ISSTA, ACM, New York, NY, USA (1998). https:\/\/doi.org\/10.1145\/271771.271800","DOI":"10.1145\/271771.271800"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 165\u2013174. PLDI 2015, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737975","DOI":"10.1145\/2737924.2737975"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Jensen, C.S., M\u00f8ller, A., Raychev, V., Dimitrov, D., Vechev, M.T.: Stateless model checking of event-driven applications. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 57\u201373. OOPSLA 2015, ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2814270.2814282","DOI":"10.1145\/2814270.2814282"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Jonsson, B., L\u00e5ng, M., Sagonas, K.: Awaiting for godot: stateless model checking that avoids executions where nothing happens. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, pp. 284\u2013293. FMCAD 2022, IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_35","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_35"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"K\u00e4hk\u00f6nen, K., Saarikivi, O., Heljanko, K.: Using unfoldings in automated testing of multithreaded programs. In: IEEE\/ACM International Conference on Automated Software Engineering, pp. 150\u2013159. ASE\u201912, ACM, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2351676.2351698, http:\/\/dl.acm.org\/citation.cfm?id=2351676","DOI":"10.1145\/2351676.2351698"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-85361-9_21","volume-title":"CONCUR 2008 - Concurrency Theory","author":"H Kastenberg","year":"2008","unstructured":"Kastenberg, H., Rensink, A.: Dynamic partial order reduction using probe sets. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 233\u2013247. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_21"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM on Program. Lang. 2(POPL), 17:1\u201317:32 (2018). https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Marmanis, I., Gladstein, V., Vafeiadis, V.: Truly stateless, optimal dynamic partial order reduction. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498711","DOI":"10.1145\/3498711"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 96\u2013110. PLDI 2019, ACM, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","DOI":"10.1145\/3314221.3314609"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Ren, X., Vafeiadis, V.: Dynamic partial order reductions for Spinloops. In: Formal Methods in Computer Aided Design, pp. 163\u2013172. FMCAD 2021, IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_25","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_25"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the Linux kernel\u2019s read-copy update (RCU). Softw. Tools Technol. Transf. 21(3), 287\u2013306 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00514-6","DOI":"10.1007\/s10009-019-00514-6"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Vafeiadis, V.: HMC: model checking for hardware memory models. In: Larus, J.R., Ceze, L., Strauss, K. (eds.) Architectural Support for Programming Languages and Operating Systems, pp. 1157\u20131171. ASPLOS \u201920, ACM (2020). https:\/\/doi.org\/10.1145\/3373376.3378480","DOI":"10.1145\/3373376.3378480"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-030-81685-8_20","volume-title":"Computer Aided Verification","author":"M Kokologiannakis","year":"2021","unstructured":"Kokologiannakis, M., Vafeiadis, V.: GenMC: a model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 427\u2013440. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-662-49674-9_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Maiya","year":"2016","unstructured":"Maiya, P., Gupta, R., Kanade, A., Majumdar, R.: Partial order reduction for event-driven multi-threaded programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 680\u2013697. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_44"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278\u2013324. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_30"},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: A technique of a state space search based on unfolding. Formal Methods Syst. Des. 6(1), 45\u201365 (1995). https:\/\/doi.org\/10.1007\/BF01384314","DOI":"10.1007\/BF01384314"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 446\u2013455. PLDI 2007, ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785"},{"key":"2_CR39","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, pp. 267\u2013280. OSDI \u201908, USENIX Association, Berkeley, CA, USA (2008). http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855760"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-96142-2_22","volume-title":"Computer Aided Verification","author":"HTT Nguyen","year":"2018","unstructured":"Nguyen, H.T.T., Rodr\u00edguez, C., Sousa, M., Coti, C., Petrucci, L.: Quasi-optimal partial order reduction. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 354\u2013371. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_22"},{"key":"2_CR41","doi-asserted-by":"publisher","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking C\/C++11 code. ACM Trans. Program. Lang. Syst. 38(3), 10:1\u201310:51 (2016). https:\/\/doi.org\/10.1145\/2806886","DOI":"10.1145\/2806886"},{"key":"2_CR42","doi-asserted-by":"publisher","unstructured":"Palmer, R., Gopalakrishnan, G., Kirby, R.M.: Semantics driven dynamic partial-order reduction of MPI-based parallel programs. In: Ur, S., Farchi, E. (eds.) Proceedings of the 5th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, pp. 43\u201353. PADTAD 2007, ACM (2007). https:\/\/doi.org\/10.1145\/1273647.1273657","DOI":"10.1145\/1273647.1273657"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: 26th International Conference on Concurrency Theory (CONCUR 2015). LIPIcs, vol.\u00a042, pp. 456\u2013469. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.456","DOI":"10.4230\/LIPIcs.CONCUR.2015.456"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-540-70889-6_13","volume-title":"Hardware and Software, Verification and Testing","author":"K Sen","year":"2007","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 166\u2013182. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70889-6_13"},{"key":"2_CR45","unstructured":"SV-COMP: Competition on Software Verification (2019). https:\/\/sv-comp.sosy-lab.org\/2019. Accessed 24 Mar 2019"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"S Tasharofi","year":"2012","unstructured":"Tasharofi, S., Karmani, R.K., Lauterburg, S., Legay, A., Marinov, D., Agha, G.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 219\u2013234. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14"},{"key":"2_CR47","doi-asserted-by":"publisher","unstructured":"Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using controlled schedulers: An empirical study. ACM Trans. Parallel Comput. 2(4), 23:1\u201323:37 (2016). https:\/\/doi.org\/10.1145\/2858651","DOI":"10.1145\/2858651"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Programming Language Design and Implementation (PLDI), pp. 250\u2013259. ACM, New York, NY, USA (2015). https:\/\/doi.org\/10.1145\/2737924.2737956","DOI":"10.1145\/2737924.2737956"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65630-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:02:13Z","timestamp":1721858533000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}