{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:20:09Z","timestamp":1743132009950,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031737503"},{"type":"electronic","value":"9783031737510"}],"license":[{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-73751-0_8","type":"book-chapter","created":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T23:02:38Z","timestamp":1729638158000},"page":"79-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Trading Space for\u00a0Simplicity in\u00a0Stateless Model Checking"],"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,10,23]]},"reference":[{"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, POPL 2014, pp. 373\u2013384. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535845","key":"8_CR1","DOI":"10.1145\/2535838.2535845"},{"key":"8_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"},{"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","key":"8_CR3","DOI":"10.1145\/3073408"},{"key":"8_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-031-45332-8_9","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2023","unstructured":"Abdulla, P.A., et al.: Tailoring stateless model checking for event-driven multi-threaded programs. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023, Part II. LNCS, vol. 14216, pp. 176\u2013198. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_9"},{"doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Das, S., Jonsson, B., Sagonas, K.: Parsimonious optimal dynamic partial order reduction. CoRR abs\/2405.11128 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.11128","key":"8_CR5","DOI":"10.48550\/ARXIV.2405.11128"},{"key":"8_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-031-65630-9_2","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2024","unstructured":"Abdulla, P.A., Atig, M.F., Das, S., Jonsson, B., Sagonas, K.: Parsimonious optimal dynamic partial order reduction. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024, Part II. LNCS, vol. 14682, pp. 19\u201343. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_2"},{"issue":"2","key":"8_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"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, ICST 2013, Los Alamitos, CA, USA, pp. 154\u2013163. IEEE (2013). https:\/\/doi.org\/10.1109\/ICST.2013.50","key":"8_CR8","DOI":"10.1109\/ICST.2013.50"},{"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 (2005). https:\/\/doi.org\/10.1145\/1040305.1040315","key":"8_CR9","DOI":"10.1145\/1040305.1040315"},{"doi-asserted-by":"publisher","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Ph.D. thesis, University of Li\u00e8ge (1996). https:\/\/doi.org\/10.1007\/3-540-60761-7. http:\/\/www.springer.com\/gp\/book\/9783540607618, also, volume\u00a01032 of LNCS, Springer","key":"8_CR10","DOI":"10.1007\/3-540-60761-7"},{"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 (1997). https:\/\/doi.org\/10.1145\/263699.263717","key":"8_CR11","DOI":"10.1145\/263699.263717"},{"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","key":"8_CR12","DOI":"10.1007\/s10703-005-1489-x"},{"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, ISSTA, pp. 124\u2013133. ACM, New York (1998). https:\/\/doi.org\/10.1145\/271771.271800","key":"8_CR13","DOI":"10.1145\/271771.271800"},{"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, OOPSLA 2015, pp. 57\u201373. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2814270.2814282","key":"8_CR14","DOI":"10.1145\/2814270.2814282"},{"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, FMCAD 2022, pp. 284\u2013293. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_35","key":"8_CR15","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_35"},{"key":"8_CR16","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"},{"doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2(POPL), 17:1\u201317:32 (2018). https:\/\/doi.org\/10.1145\/3158105","key":"8_CR17","DOI":"10.1145\/3158105"},{"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","key":"8_CR18","DOI":"10.1145\/3498711"},{"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, PLDI 2019, pp. 96\u2013110. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314609","key":"8_CR19","DOI":"10.1145\/3314221.3314609"},{"doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Ren, X., Vafeiadis, V.: Dynamic partial order reductions for spinloops. In: Formal Methods in Computer Aided Design, FMCAD 2021, pp. 163\u2013172. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_25","key":"8_CR20","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_25"},{"doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Sagonas, K.: Stateless model checking of the Linux kernel\u2019s read\u2013copy update (RCU). Softw. Tools Technol. Transf. 21(3), 287\u2013306 (2019). https:\/\/doi.org\/10.1007\/s10009-019-00514-6","key":"8_CR21","DOI":"10.1007\/s10009-019-00514-6"},{"key":"8_CR22","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, Part I. LNCS, vol. 12759, pp. 427\u2013440. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20"},{"issue":"9","key":"8_CR23","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans. Comput."},{"issue":"2\u20133","key":"8_CR24","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1023\/A:1025132427497","volume":"25","author":"KG Larsen","year":"2003","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Compact data structures and statespace reduction for model-checking real-time systems. Real Time Syst. 25(2\u20133), 255\u2013275 (2003). https:\/\/doi.org\/10.1023\/A:1025132427497","journal-title":"Real Time Syst."},{"issue":"1\u20132","key":"8_CR25","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/S100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/S100090050010","journal-title":"Softw. Tools Technol. Transf."},{"key":"8_CR26","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":"8_CR27","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"},{"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, OSDI 2008, pp. 267\u2013280. USENIX Association, Berkeley (2008). http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855760","key":"8_CR28"},{"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, PADTAD 2007, pp. 43\u201353. ACM (2007). https:\/\/doi.org\/10.1145\/1273647.1273657","key":"8_CR29","DOI":"10.1145\/1273647.1273657"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-61550-4_141","volume-title":"Mathematical Foundations of Computer Science 1996","author":"D Peled","year":"1996","unstructured":"Peled, D.: Partial order reduction: model-checking using representatives. In: Penczek, W., Sza\u0142as, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 93\u2013112. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61550-4_141"},{"key":"8_CR31","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"},{"doi-asserted-by":"publisher","unstructured":"Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification, Proceedings of a DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a029, pp. 213\u2013231. DIMACS\/AMS (1996). https:\/\/doi.org\/10.1090\/DIMACS\/029\/12","key":"8_CR32","DOI":"10.1090\/DIMACS\/029\/12"},{"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 (2015). https:\/\/doi.org\/10.1145\/2737924.2737956","key":"8_CR33","DOI":"10.1145\/2737924.2737956"}],"container-title":["Lecture Notes in Computer Science","Real Time and Such"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-73751-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T23:03:19Z","timestamp":1729638199000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-73751-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,23]]},"ISBN":["9783031737503","9783031737510"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-73751-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,23]]},"assertion":[{"value":"23 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}