{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:57:15Z","timestamp":1781132235400,"version":"3.54.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032281869","type":"print"},{"value":"9783032281876","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-28187-6_5","type":"book-chapter","created":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:04:17Z","timestamp":1781129057000},"page":"74-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Sound Automatic Lock Placement for\u00a0Concurrent Programs with\u00a0Pointers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7664-5828","authenticated-orcid":false,"given":"Nicolas","family":"Waldburger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5792-0658","authenticated-orcid":false,"given":"Florian","family":"Faissole","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4800-9011","authenticated-orcid":false,"given":"Ryo","family":"Okabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4078-3591","authenticated-orcid":false,"given":"Denis","family":"Cousineau","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,11]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Berry, G.: SCADE: synchronous design and validation of embedded control software. In: Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, pp. 19\u201333 (2007). https:\/\/doi.org\/10.1007\/978-1-4020-6254-4_2","DOI":"10.1007\/978-1-4020-6254-4_2"},{"key":"5_CR2","unstructured":"Boehm, H.J.: How to miscompile programs with \u201cbenign\u201d data races. In: 3rd USENIX Workshop on Hot Topics in Parallelism (HotPar 2011) (2011). https:\/\/www.usenix.org\/conference\/hotpar-11\/how-miscompile-programs-benign-data-races"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Carr\u00e9, B., Garnsworthy, J.: SPARK\u2014an annotated Ada subset for safety-critical programming. In: Proceedings of the conference on TRI-ADA 1990, pp. 392\u2013402. TRI-Ada 1990 (1990). https:\/\/doi.org\/10.1145\/255471.255563. https:\/\/dl.acm.org\/doi\/10.1145\/255471.255563","DOI":"10.1145\/255471.255563"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 304\u2013315 (2008). https:\/\/doi.org\/10.1145\/1375581.1375619","DOI":"10.1145\/1375581.1375619"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Conchon, S., Filli\u00e2tre, J.: A persistent union-find data structure. In: Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, 5 October 2007, pp. 37\u201346 (2007). https:\/\/doi.org\/10.1145\/1292535.1292541","DOI":"10.1145\/1292535.1292541"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Dac\u00edk, T., Vojnar, T.: RacerF: Lightweight Static Data Race Detection for C Code (2025). https:\/\/doi.org\/10.48550\/arXiv.2502.04905. http:\/\/arxiv.org\/abs\/2502.04905","DOI":"10.48550\/arXiv.2502.04905"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. ACM SIGPLAN Not. 42(1), 291\u2013296 (2007). https:\/\/doi.org\/10.1145\/1190215.1190260. https:\/\/dl.acm.org\/doi\/10.1145\/1190215.1190260","DOI":"10.1145\/1190215.1190260"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Gerakios, P., Papaspyrou, N., Sagonas, K.: Race-free and memory-safe multithreading: design and implementation in cyclone. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2010, pp. 15\u201326 (2010). https:\/\/doi.org\/10.1145\/1708016.1708020","DOI":"10.1145\/1708016.1708020"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Grossman, D.: Type-safe multithreading in cyclone. In: Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI 2003, pp. 13\u201325 (2003). https:\/\/doi.org\/10.1145\/604174.604177","DOI":"10.1145\/604174.604177"},{"key":"5_CR11","unstructured":"Hicks, M., Foster, J.S., Pratikakis, P.: Lock inference for atomic sections. In: Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, p.\u00a013 (2006)"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Kirchner, F., Kosmatov, N., Pr\u00e9vosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7. https:\/\/cea.hal.science\/cea-01808981","DOI":"10.1007\/s00165-014-0326-7"},{"key":"5_CR13","unstructured":"Le\u00a0Gall, T., Rochel, J., Faissole, F., Signoles, J., Cousineau, D.: Alias: pointeurs espionn\u00e9s en s\u00e9rie. In: 35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024), pp. 85\u2013104 (2024). https:\/\/hal.science\/hal-04407140"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Lin, Y., Kulkarni, S.S.: Automatic repair for multi-threaded programs with deadlock\/livelock using maximum satisfiability. In: International Symposium on Software Testing and Analysis, ISSTA 2014, San Jose, CA, USA - 21\u201326 July 2014, pp. 237\u2013247 (2014). https:\/\/doi.org\/10.1145\/2610384.2610398","DOI":"10.1145\/2610384.2610398"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 329\u2013339. ASPLOS XIII (2008). https:\/\/doi.org\/10.1145\/1346281.1346323","DOI":"10.1145\/1346281.1346323"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Matsakis, N.D., Klock, F.S.: The rust language. Ada Lett. 34(3), 103\u2013104 (2014). https:\/\/doi.org\/10.1145\/2692956.2663188","DOI":"10.1145\/2692956.2663188"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.: Autolocker: synchronization inference for atomic sections. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pp. 346\u2013358 (2006). https:\/\/doi.org\/10.1145\/1111037.1111068","DOI":"10.1145\/1111037.1111068"},{"key":"5_CR18","unstructured":"Min\u00e9, A., et al.: Taking static analysis to the next level: proving the absence of run-time errors and data races with Astr\u00e9e. In: 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016) (2016). https:\/\/hal.science\/hal-01271552"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Rugina, R., Rinard, M.: Pointer analysis for multithreaded programs. In: Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation, PLDI 1999, pp. 77\u201390 (1999). https:\/\/doi.org\/10.1145\/301618.301645. https:\/\/dl.acm.org\/doi\/10.1145\/301618.301645","DOI":"10.1145\/301618.301645"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Rugina, R., Rinard, M.C.: Pointer analysis for structured parallel programs. ACM Trans. Program. Lang. Syst. 25(1), 70\u2013116 (2003). https:\/\/doi.org\/10.1145\/596980.596982. https:\/\/dl.acm.org\/doi\/10.1145\/596980.596982","DOI":"10.1145\/596980.596982"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: Proceedings of the Eighth ACM SIGPLAN Symposium on Principles and Practices of Parallel Programming, PPoPP 2001, pp. 12\u201323 (2001). https:\/\/doi.org\/10.1145\/379539.379553. https:\/\/dl.acm.org\/doi\/10.1145\/379539.379553","DOI":"10.1145\/379539.379553"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Steensgaard, B.: Points-to analysis in almost linear time. In: Conference Record of POPL\u201996: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, St. Petersburg Beach, Florida, USA, 21\u201324 January 1996, pp. 32\u201341 (1996). https:\/\/doi.org\/10.1145\/237721.237727","DOI":"10.1145\/237721.237727"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Sui, Y., Di, P., Xue, J.: Sparse flow-sensitive pointer analysis for multithreaded programs. In: Proceedings of the 2016 International Symposium on Code Generation and Optimization, CGO 2016, pp. 160\u2013170. (2016). https:\/\/doi.org\/10.1145\/2854038.2854043. https:\/\/dl.acm.org\/doi\/10.1145\/2854038.2854043","DOI":"10.1145\/2854038.2854043"},{"key":"5_CR24","unstructured":"Vojdani, V., Vene, V.: Goblint: path-sensitive data race analysis. In: Annales Univ. Sci. Budapest., Sect. Comp. vol.\u00a030, pp. 141\u2013155 (2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28187-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T22:04:19Z","timestamp":1781129059000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28187-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032281869","9783032281876"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28187-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"11 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Urbino","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"46","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2026\/forte","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}