{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:57:51Z","timestamp":1743109071052,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031673207"},{"type":"electronic","value":"9783031673214"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-67321-4_8","type":"book-chapter","created":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T16:02:07Z","timestamp":1724515327000},"page":"124-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Static Data Race Detection via\u00a0Lazy Sequentialization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1815-218X","authenticated-orcid":false,"given":"Bernd","family":"Fischer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2836-4434","authenticated-orcid":false,"given":"Giulio","family":"Garbi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4978-4307","authenticated-orcid":false,"given":"Salvatore","family":"La Torre","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8697-2980","authenticated-orcid":false,"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5713-1381","authenticated-orcid":false,"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,25]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/S10009-017-0469-Y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/S10009-017-0469-Y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Blackshear, S., Gorogiannis, N., O\u2019Hearn, P.W., Sergey, I.: RacerD: compositional static race detection. Proc. ACM Program. Lang. 2(OOPSLA), 144:1\u2013144:28 (2018). https:\/\/doi.org\/10.1145\/3276514","DOI":"10.1145\/3276514"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Chaki, S., Gurfinkel, A., Sinha, N.: Efficient verification of periodic programs using sequential consistency and snapshots. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 51\u201358. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987595","DOI":"10.1109\/FMCAD.2014.6987595"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-99527-0_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Coto","year":"2022","unstructured":"Coto, A., Inverso, O., Sales, E., Tuosto, E.: A prototype for data race detection in CSeq 3. In: TACAS 2022, Part II. LNCS, vol. 13244, pp. 413\u2013417. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_23"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Currie, D.W., Hu, A.J., Rajan, S.P.: Automatic formal verification of DSP software. In: Micheli, G.D. (ed.) Proceedings of the 37th Conference on Design Automation, Los Angeles, CA, USA, 5\u20139 June 2000, pp. 130\u2013135. ACM (2000). https:\/\/doi.org\/10.1145\/337292.337339","DOI":"10.1145\/337292.337339"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26-28 January 2011, pp. 411\u2013422. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926432","DOI":"10.1145\/1926385.1926432"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Fischer, B., La Torre, S., Parlato, G., Schrammel, P.: CBMC-SSM: bounded model checking of C programs with symbolic shadow memory. In: 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, 10\u201314 October 2022, pp. 156:1\u2013156:5. ACM (2022). https:\/\/doi.org\/10.1145\/3551349.3559523","DOI":"10.1145\/3551349.3559523"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-662-54580-5_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Greitschus","year":"2017","unstructured":"Greitschus, M., Dietsch, D., Heizmann, M., Nutz, A., Sch\u00e4tzle, C., Schilling, C., Sch\u00fcssele, F., Podelski, A.: Ultimate Taipan: trace abstraction and abstract interpretation. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part II. LNCS, vol. 10206, pp. 399\u2013403. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_31"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-030-99527-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F He","year":"2022","unstructured":"He, F., Sun, Z., Fan, H.: Deagle: an SMT-based verifier for multi-threaded programs (Competition Contribution). In: TACAS 2022, Part II. LNCS, vol. 13244, pp. 424\u2013428. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_25"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-89963-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2018","unstructured":"Heizmann, M., et al.: Ultimate Automizer and the search for perfect interpolants. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part II. LNCS, vol. 10806, pp. 447\u2013451. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-319-08867-9_39","volume-title":"Computer Aided Verification","author":"O Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585\u2013602. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_39"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded verification of multi-threaded programs via lazy sequentialization. ACM Trans. Program. Lang. Syst. 44(1), 1:1\u20131:50 (2022). https:\/\/doi.org\/10.1145\/3478536","DOI":"10.1145\/3478536"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Kahlon, V., Sinha, N., Kruus, E., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: van Vliet, H., Issarny, V. (eds.) Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, 24\u201328 August 2009, pp. 13\u201322. ACM (2009). https:\/\/doi.org\/10.1145\/1595696.1595701","DOI":"10.1145\/1595696.1595701"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-030-99527-0_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Klumpp","year":"2022","unstructured":"Klumpp, D., et al.: Ultimate GemCutter and the axes of generalization. In: TACAS 2022, Part II. LNCS, vol. 13244, pp. 479\u2013483. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_35"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S La Torre","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477\u2013492. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73\u201397 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0078-9","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-030-45237-7_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Ponce-de-Le\u00f3n","year":"2020","unstructured":"Ponce-de-Le\u00f3n, H., Furbach, F., Heljanko, K., Meyer, R.: Dartagnan: bounded model checking for weak memory models (Competition Contribution). In: TACAS 2020, Part II. LNCS, vol. 12079, pp. 378\u2013382. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_24"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, 10\u201313 June 2007, pp. 446\u2013455. ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-319-46520-3_12","volume-title":"Automated Technology for Verification and Analysis","author":"TL Nguyen","year":"2016","unstructured":"Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for the safety verification of unbounded concurrent programs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 174\u2013191. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_12"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., La Torre, S., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proc. of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pp. 753\u2013764. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115686","DOI":"10.1109\/ASE.2017.8115686"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: LOCKSMITH: Practical static race detection for C. ACM Trans. Program. Lang. Syst. 33(1), 3:1\u20133:55 (2011). https:\/\/doi.org\/10.1145\/1889997.1890000","DOI":"10.1145\/1889997.1890000"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Pugh, W.W., Chambers, C. (eds.) Proc. of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, Washington, DC, USA, 9\u201311 June 2004, pp. 14\u201324. ACM (2004). https:\/\/doi.org\/10.1145\/996841.996845","DOI":"10.1145\/996841.996845"},{"issue":"4","key":"8_CR24","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391\u2013411 (1997). https:\/\/doi.org\/10.1145\/265924.265927","journal-title":"ACM Trans. Comput. Syst."},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-53288-8_18","volume-title":"Computer Aided Verification","author":"D Schemmel","year":"2020","unstructured":"Schemmel, D., B\u00fcning, J., Rodr\u00edguez, C., Laprell, D., Wehrle, K.: Symbolic partial-order execution for testing multi-threaded programs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 376\u2013400. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_18"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-29860-8_9","volume-title":"Runtime Verification","author":"K Serebryany","year":"2012","unstructured":"Serebryany, K., Potapenko, A., Iskhodzhanov, T., Vyukov, D.: Dynamic race detection with LLVM compiler. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 110\u2013114. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_9"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-662-46681-0_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Tomasco","year":"2015","unstructured":"Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Verifying concurrent programs by memory unwinding. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 551\u2013565. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_52"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-319-66197-1_12","volume-title":"Software Engineering and Formal Methods","author":"E Tomasco","year":"2017","unstructured":"Tomasco, E., Nguyen, T.L., Fischer, B., La\u00a0Torre, S., Parlato, G.: Using shared memory abstractions to design eager sequentializations for weak memory\u00a0models. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 185\u2013202. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_12"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, 3\u20137 September 2016, pp. 391\u2013402. ACM (2016). https:\/\/doi.org\/10.1145\/2970276.2970337","DOI":"10.1145\/2970276.2970337"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007, Dubrovnik, Croatia, 3\u20137 September 2007, pp. 205\u2013214. ACM (2007). https:\/\/doi.org\/10.1145\/1287624.1287654","DOI":"10.1145\/1287624.1287654"},{"key":"8_CR31","unstructured":"Vyukov, D.: Bug with a context switch bound 5. https:\/\/social.msdn.microsoft.com\/Forums\/en-US\/91c1971c-519f-4ad2-816d-149e6b2fd916\/bug-with-a-context-switch-bound-5?forum=chess (2010). Accessed 17 Aug 2022"}],"container-title":["Lecture Notes in Computer Science","Networked Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-67321-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,24]],"date-time":"2024-08-24T16:02:55Z","timestamp":1724515375000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-67321-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031673207","9783031673214"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-67321-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"NETYS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Networked Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rabat","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","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":"29 May 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 May 2024","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":"netys2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/netys.net\/committees\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}