{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:36:19Z","timestamp":1768282579243,"version":"3.49.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T00:00:00Z","timestamp":1735344000000},"content-version":"vor","delay-in-days":27,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005713","name":"Technische Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Thread-modular approaches to static analysis help mitigate the state space explosion encountered when analyzing multi-threaded programs. This is enabled by abstracting away some aspects of interactions between threads. We propose the notion of <jats:italic>concurrency-sensitivity<\/jats:italic>, which determines how an analysis takes the computation history of a multi-threaded program into account to exclude spurious thread interactions. Just as for other form of sensitivity, such as flow-, context, and path-sensitivity, there is a trade-off to be made between precision and scalability. The choice of concurrency-sensitivity is typically hard-coded into the analysis. However, the suitability of a chosen sensitivity hinges on the program and property to be analyzed. We thus propose to decouple the concurrency-sensitivity from the analysis and realize this in a generic framework. The framework allows for the seamless incorporation of custom abstractions of the computation history of a thread, so-called <jats:italic>digests<\/jats:italic>, to exclude spurious thread interactions. While <jats:italic>concrete<\/jats:italic> digests track properties precisely, the framework enables further abstraction through <jats:italic>abstract<\/jats:italic> digests. These may decrease analysis cost while hopefully retaining precision for the property of interest. We propose digests that, e.g., track held mutexes, thread IDs, or observed events. Digests tailored to programming language features, such as condition variables or recursive mutexes, highlight the framework\u2019s versatility.<\/jats:p>","DOI":"10.1007\/s10009-024-00773-y","type":"journal-article","created":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T08:32:33Z","timestamp":1735374753000},"page":"727-746","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["The digest framework: concurrency-sensitivity for abstract interpretation"],"prefix":"10.1007","volume":"26","author":[{"given":"Michael","family":"Schwarz","sequence":"first","affiliation":[]},{"given":"Julian","family":"Erhard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,12,28]]},"reference":[{"key":"773_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1145\/1229428.1229471","volume-title":"PPoPP\u00a0\u201907","author":"S. Agarwal","year":"2007","unstructured":"Agarwal, S., Barik, R., Sarkar, V., Shyamasundar, R.K.: May-happen-in-parallel analysis of x10 programs. In: PPoPP\u00a0\u201907, pp.\u00a0183\u2013193. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1229428.1229471"},{"key":"773_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-30793-5_3","volume-title":"Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings","author":"E. Albert","year":"2012","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S.: Analysis of may-happen-in-parallel in concurrent objects. In: Giese, H., Rosu, G. (eds.) Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings. Lecture Notes in Computer Science, vol.\u00a07273, pp.\u00a035\u201351. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-30793-5_3"},{"key":"773_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-662-48288-9_5","volume-title":"Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings","author":"E. Albert","year":"2015","unstructured":"Albert, E., Genaim, S., Gordillo, P.: May-happen-in-parallel analysis for asynchronous programs with inter-procedural synchronization. In: Blazy, S., Jensen, T.P. (eds.) Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09291, pp.\u00a072\u201389. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_5"},{"key":"773_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-68167-2_3","volume-title":"Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings","author":"E. Albert","year":"2017","unstructured":"Albert, E., Genaim, S., Gordillo, P.: May-happen-in-parallel analysis with returned futures. In: D\u2019Souza, D., Kumar, K.N. (eds.) Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings. Lecture Notes in Computer Science, vol.\u00a010482, pp.\u00a042\u201358. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_3"},{"key":"773_CR5","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-35182-2_12","volume-title":"APLAS \u201912","author":"K. Apinis","year":"2012","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a Swiss army knife for program analysis. In: APLAS \u201912, pp.\u00a0157\u2013172. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_12"},{"key":"773_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-69330-7_11","volume-title":"LCPC\u00a0\u201906","author":"R. Barik","year":"2006","unstructured":"Barik, R.: Efficient computation of may-happen-in-parallel information for concurrent Java programs. In: LCPC\u00a0\u201906. LNCS, vol.\u00a04339, pp.\u00a0152\u2013169. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/978-3-540-69330-7_11"},{"issue":"6","key":"773_CR7","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/267896.267921","volume":"22","author":"R. Bod\u00edk","year":"1997","unstructured":"Bod\u00edk, R., Gupta, R., Soffa, M.L.: Refining data flow information using infeasible paths. SIGSOFT Softw. Eng. Notes 22(6), 361\u2013377 (1997). https:\/\/doi.org\/10.1145\/267896.267921","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"773_CR8","volume-title":"Programming with POSIX Threads","author":"D.R. Butenhof","year":"1993","unstructured":"Butenhof, D.R.: Programming with POSIX Threads. Addison-Wesley Professional (1993)"},{"key":"773_CR9","unstructured":"Cai, Y., Yao, P., Ye, C., Zhang, C.: Place your locks well: understanding and detecting lock misuse bugs. In: Calandrino, J.A., Troncoso, C. (eds.) 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9\u201311, 2023, pp.\u00a03727\u20133744. USENIX Association (2023). https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/cai-yuandao"},{"key":"773_CR10","series-title":"EPTCS","doi-asserted-by":"publisher","first-page":"325","DOI":"10.4204\/EPTCS.129.19","volume-title":"Semantics, Abstract Interpretation, and Reasoning About Programs: Essays Dedicated to David A. Schmidt on the Occasion of His Sixtieth Birthday","author":"A. Cortesi","year":"2013","unstructured":"Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Banerjee, A., Danvy, O., Doh, K., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning About Programs: Essays Dedicated to David A. Schmidt on the Occasion of His Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013. EPTCS, vol.\u00a0129, pp.\u00a0325\u2013336 (2013). https:\/\/doi.org\/10.4204\/EPTCS.129.19"},{"key":"773_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/567752.567778","volume-title":"Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp.\u00a0269\u2013282. ACM Press (1979). https:\/\/doi.org\/10.1145\/567752.567778"},{"key":"773_CR12","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/512529.512538","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"M. Das","year":"2002","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: Knoop, J., Hendren, L.J. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pp.\u00a057\u201368. ACM (2002). https:\/\/doi.org\/10.1145\/512529.512538"},{"key":"773_CR13","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/J.SCICO.2018.05.001","volume":"163","author":"P. de Carvalho Gomes","year":"2018","unstructured":"de Carvalho Gomes, P., Gurov, D., Huisman, M., Artho, C.: Specification and verification of synchronization with condition variables. Sci. Comput. Program. 163, 174\u2013189 (2018). https:\/\/doi.org\/10.1016\/J.SCICO.2018.05.001","journal-title":"Sci. Comput. Program."},{"key":"773_CR14","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1109\/ICPP.2015.98","volume-title":"ICPP","author":"P. Di","year":"2015","unstructured":"Di, P., Sui, Y., Ye, D., Xue, J.: Region-based may-happen-in-parallel analysis for C programs. In: ICPP, pp.\u00a0889\u2013898. IEEE (2015). https:\/\/doi.org\/10.1109\/ICPP.2015.98"},{"key":"773_CR15","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/945445.945468","volume-title":"Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003","author":"D.R. Engler","year":"2003","unstructured":"Engler, D.R., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. In: Scott, M.L., Peterson, L.L. (eds.) Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pp.\u00a0237\u2013252. ACM (2003). https:\/\/doi.org\/10.1145\/945445.945468"},{"key":"773_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-79124-9_9","volume-title":"Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings","author":"P. Ferrara","year":"2008","unstructured":"Ferrara, P.: Static analysis via abstract interpretation of the happens-before memory model. In: Beckert, B., H\u00e4hnle, R. (eds.) Tests and Proofs - 2nd International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a04966, pp.\u00a0116\u2013133. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_9"},{"issue":"1\u20132","key":"773_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(98)00194-7","volume":"216","author":"R. Giacobazzi","year":"1999","unstructured":"Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci. 216(1\u20132), 159\u2013211 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00194-7","journal-title":"Theor. Comput. Sci."},{"key":"773_CR18","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-49727-7_12","volume-title":"Static Analysis","author":"M. Handjieva","year":"1998","unstructured":"Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) Static Analysis, pp.\u00a0200\u2013214. Springer, Berlin (1998). https:\/\/doi.org\/10.1007\/3-540-49727-7_12"},{"key":"773_CR19","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/567446.567454","volume-title":"Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201980","author":"L.H. Holley","year":"1980","unstructured":"Holley, L.H., Rosen, B.K.: Qualified data flow problems. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201980, pp.\u00a068\u201382. Association for Computing Machinery, New York (1980). https:\/\/doi.org\/10.1145\/567446.567454"},{"issue":"4","key":"773_CR20","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2629608","volume":"36","author":"A. Kaiser","year":"2014","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 14:1\u201314:29 (2014). https:\/\/doi.org\/10.1145\/2629608","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"773_CR21","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/3230624","volume":"40","author":"S. Kim","year":"2018","unstructured":"Kim, S., Rival, X., Ryu, S.: A theoretical foundation of sensitivity in an abstract interpretation framework. ACM Trans. Program. Lang. Syst. 40(3), 13:1\u201313:44 (2018). https:\/\/doi.org\/10.1145\/3230624","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"773_CR22","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L. Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) Programming Languages and Systems, pp.\u00a05\u201320. Springer, Berlin (2005)"},{"issue":"1","key":"773_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:26)2012","volume":"8","author":"A. Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Log. Methods Comput. Sci. 8(1), 1\u201363 (2012). https:\/\/doi.org\/10.2168\/LMCS-8(1:26)2012","journal-title":"Log. Methods Comput. Sci."},{"key":"773_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-54013-4_3","volume-title":"VMCAI\u00a0\u201914","author":"A. Min\u00e9","year":"2014","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: VMCAI\u00a0\u201914. LNCS, vol.\u00a08318, pp.\u00a039\u201358. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_3"},{"key":"773_CR25","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1109\/EMSOFT.2015.7318261","volume-title":"International Conference on Embedded Software, EMSOFT 2015","author":"A. Min\u00e9","year":"2015","unstructured":"Min\u00e9, A., Delmas, D.: Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software. In: Girault, A., Guan, N. (eds.) International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4-9, 2015, pp.\u00a065\u201374. IEEE (2015). https:\/\/doi.org\/10.1109\/EMSOFT.2015.7318261"},{"key":"773_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-52234-0_21","volume-title":"VMCAI\u00a0\u201917","author":"R. Monat","year":"2017","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: VMCAI\u00a0\u201917. LNCS, vol.\u00a010145, pp.\u00a0386\u2013404. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_21"},{"key":"773_CR27","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1145\/3453483.3454057","volume-title":"PLDI \u201921","author":"B. Montagu","year":"2021","unstructured":"Montagu, B., Jensen, T.: Trace-based control-flow analysis. In: PLDI \u201921, pp.\u00a0482\u2013496. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3453483.3454057"},{"key":"773_CR28","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-66706-5_13","volume-title":"SAS\u00a0\u201917","author":"S. Mukherjee","year":"2017","unstructured":"Mukherjee, S., Padon, O., Shoham, S., D\u2019Souza, D., Rinetzky, N.: Thread-local semantics and its efficient sequential abstractions for race-free programs. In: SAS\u00a0\u201917. LNCS, vol.\u00a01042, pp.\u00a0253\u2013276. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_13"},{"key":"773_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-48166-4_21","volume-title":"ESEC\/FSE \u201999","author":"G. Naumovich","year":"1999","unstructured":"Naumovich, G., Avrunin, G.S., Clarke, L.A.: An efficient algorithm for computing mhp information for concurrent Java programs. In: ESEC\/FSE \u201999. LNCS, vol.\u00a01687, pp.\u00a0338\u2013354. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-48166-4_21"},{"issue":"7","key":"773_CR30","doi-asserted-by":"publisher","first-page":"149:1","DOI":"10.1145\/3464457","volume":"54","author":"J. Park","year":"2022","unstructured":"Park, J., Lee, H., Ryu, S.: A survey of parametric static analysis. ACM Comput. Surv. 54(7), 149:1\u2013149:37 (2022). https:\/\/doi.org\/10.1145\/3464457","journal-title":"ACM Comput. Surv."},{"issue":"3","key":"773_CR31","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1137\/0205035","volume":"5","author":"G.D. Plotkin","year":"1976","unstructured":"Plotkin, G.D.: A powerdomain construction. SIAM J. Comput. 5(3), 452\u2013487 (1976). https:\/\/doi.org\/10.1137\/0205035","journal-title":"SIAM J. Comput."},{"key":"773_CR32","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/1133981.1134019","volume-title":"Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation","author":"P. Pratikakis","year":"2006","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.W.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Schwartzbach, M.I., Ball, T. (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pp.\u00a0320\u2013331. ACM (2006). https:\/\/doi.org\/10.1145\/1133981.1134019"},{"issue":"5","key":"773_CR33","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X. Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26\u2013es (2007). https:\/\/doi.org\/10.1145\/1275497.1275501","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"773_CR34","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 - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I","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.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a012224, pp.\u00a0376\u2013400. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_18."},{"key":"773_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-030-88806-0_18","volume-title":"Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings","author":"M. Schwarz","year":"2021","unstructured":"Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings. Lecture Notes in Computer Science, vol.\u00a012913, pp.\u00a0359\u2013383. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_18"},{"key":"773_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-031-30044-8_2","volume-title":"Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings","author":"M. Schwarz","year":"2023","unstructured":"Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings. Lecture Notes in Computer Science, vol.\u00a013990, pp.\u00a028\u201358. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_2"},{"key":"773_CR37","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-030-88806-0_19","volume-title":"Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings","author":"D. Sharma","year":"2021","unstructured":"Sharma, D., Sharma, S.: Thread-modular analysis of release-acquire concurrency. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings. LNCS, vol.\u00a012913, pp.\u00a0384\u2013404. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_19"},{"key":"773_CR38","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-030-02768-1_6","volume-title":"APLAS\u00a0\u201918","author":"T. Suzanne","year":"2018","unstructured":"Suzanne, T., Min\u00e9, A.: Relational thread-modular abstract interpretation under relaxed memory models. In: APLAS\u00a0\u201918. LNCS, vol.\u00a011275, pp.\u00a0109\u2013128. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_6"},{"key":"773_CR39","first-page":"141","volume":"30","author":"V. Vojdani","year":"2009","unstructured":"Vojdani, V., Vene, V.: Goblint: path-sensitive data race analysis. Ann. Univ. Sci. Bp. Rolando E\u00f6tv\u00f6s Nomin., Sect. Comput. 30, 141\u2013155 (2009)","journal-title":"Ann. Univ. Sci. Bp. Rolando E\u00f6tv\u00f6s Nomin., Sect. Comput."},{"key":"773_CR40","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/2970276.2970337","volume-title":"Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016","author":"V. Vojdani","year":"2016","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, September 3-7, 2016, pp.\u00a0391\u2013402. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2970276.2970337"},{"key":"773_CR41","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/1287624.1287654","volume-title":"Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007","author":"J.W. Voung","year":"2007","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, September 3-7, 2007, pp.\u00a0205\u2013214. ACM (2007). https:\/\/doi.org\/10.1145\/1287624.1287654."},{"key":"773_CR42","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/3168813","volume-title":"CGO \u201918","author":"Q. Zhou","year":"2018","unstructured":"Zhou, Q., Li, L., Wang, L., Xue, J., Feng, X.: May-happen-in-parallel analysis with static vector clocks. In: CGO \u201918, pp.\u00a0228\u2013240. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3168813"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00773-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00773-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00773-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T11:43:25Z","timestamp":1738842205000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00773-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":42,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["773"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00773-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12]]},"assertion":[{"value":"12 December 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 December 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}