{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T18:30:48Z","timestamp":1776796248153,"version":"3.51.2"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>A challenge of writing concurrent message passing programs is ensuring the absence of partial deadlocks, which can cause severe memory leaks in long running systems. Several static analysis techniques have been proposed for automatically detecting partial deadlocks in Go programs. For a large enterprise code base, we found these tools too imprecise to reason about process communication that is parametric, i.e., where the number of channel communication operations or the channel capacities are determined at runtime.<\/jats:p>\n                  <jats:p>We present a novel approach to automatically verify the absence of partial deadlocks in Go program fragments with such parametric process communication. The key idea is to translate Go fragments to a core language that is sufficiently expressive to represent real-world parametric communication patterns and can be encoded into Dafny programs annotated with postconditions enforcing partial deadlock freedom. In situations where a fragment is partial deadlock free only when the concurrency parameters satisfy certain conditions, a suitable precondition can often be inferred.<\/jats:p>\n                  <jats:p>Experimental results on a real-world code base containing 583 program fragments that are beyond the reach of existing techniques have shown that the approach can verify the absence of partial deadlocks in 145 cases. For an additional 228 cases, a nontrivial precondition is inferred that the surrounding code must satisfy to ensure partial deadlock freedom.<\/jats:p>","DOI":"10.1145\/3689784","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2070-2096","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Automated Verification of Parametric Channel-Based Process Communication"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-1714-3866","authenticated-orcid":false,"given":"Georgian-Vlad","family":"Saioc","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9697-1378","authenticated-orcid":false,"given":"Julien","family":"Lange","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, Egham, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1333-2314","authenticated-orcid":false,"given":"Anders","family":"M\u00f8ller","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","first-page":"364","volume-title":"Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures (Lecture Notes in Computer Science, Vol. 4111)","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures (Lecture Notes in Computer Science, Vol. 4111), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.). Springer, 364-387. https:\/\/doi.org\/10.1007\/11804192_17 10.1007\/11804192_17"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_3_1_4_2","first-page":"70","volume-title":"Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6538)","author":"Bradley Aaron R.","year":"2011","unstructured":"Aaron R. Bradley. 2011. SAT-Based Model Checking without Unrolling. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6538), Ranjit Jhala and David A. Schmidt (Eds.). Springer, 70-87. https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7 10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_1_5_2","first-page":"688","volume-title":"Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020","author":"Breck Jason","year":"2020","unstructured":"Jason Breck, John Cyphert, Zachary Kincaid, and Thomas W. Reps. 2020. Templates and recurrences: better together. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 688-702. https:\/\/doi.org\/10.1145\/3385412.3386035 10.1145\/3385412.3386035"},{"key":"e_1_3_1_6_2","first-page":"277","volume-title":"Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358)","author":"Cimatti Alessandro","year":"2012","unstructured":"Alessandro Cimatti and Alberto Griggio. 2012. Software Model Checking via IC3. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science, Vol. 7358), P. Madhusudan and Sanjit A. Seshia (Eds.). Springer, 277-293. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23 10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_1_7_2","first-page":"420","volume-title":"Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2725)","author":"Col\u00f3n Michael","year":"2003","unstructured":"Michael Col\u00f3n, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2725), Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Springer, 420-432. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39 10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_1_8_2","first-page":"377","volume-title":"26th IEEE International Conference on Software Analysis, Evolution and Reengineering, SANER 2019, Hangzhou, China, February 24-27, 2019","author":"Dilley Nicolas","year":"2019","unstructured":"Nicolas Dilley and Julien Lange. 2019. An Empirical Study of Messaging Passing Concurrency in Go Projects. In 26th IEEE International Conference on Software Analysis, Evolution and Reengineering, SANER 2019, Hangzhou, China, February 24-27, 2019. IEEE, 377-387. https:\/\/doi.org\/10.1109\/SANER.2019.8668036 10.1109\/SANER.2019.8668036"},{"key":"e_1_3_1_9_2","first-page":"1016","volume-title":"36th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021","author":"Dilley Nicolas","year":"2021","unstructured":"Nicolas Dilley and Julien Lange. 2021. Automated Verification of Go Programs via Bounded Model Checking. In 36th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021. IEEE, 1016-1027. https:\/\/doi.org\/10.1109\/ASE51524.2021.9678571 10.1109\/ASE51524.2021.9678571"},{"key":"e_1_3_1_10_2","first-page":"125","volume-title":"International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201811, Austin, TX, USA, October 30 - November 02, 2011","author":"Een Niklas","year":"2011","unstructured":"Niklas Een, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201811, Austin, TX, USA, October 30 - November 02, 2011, Per Bjesse and Anna Slobodova (Eds.). FMCAD Inc., 125-134. http:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"issue":"2","key":"e_1_3_1_12_2","first-page":"12:1","article-title":"Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)","volume":"6","author":"Gabet Julia","year":"2020","unstructured":"Julia Gabet and Nobuko Yoshida. 2020. Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact). Dagstuhl Artifacts Ser. 6, 2 (2020), 12:1-12:3. https:\/\/doi.org\/10.4230\/DARTS.6.2.12 10.4230\/DARTS.6.2.12","journal-title":"Dagstuhl Artifacts Ser."},{"key":"e_1_3_1_13_2","first-page":"69","volume-title":"Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8559)","author":"Garg Pranav","year":"2014","unstructured":"Pranav Garg, Christof L\u00f6ding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8559), Armin Biere and Roderick Bloem (Eds.). Springer, 69-87. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5 10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_1_15_2","first-page":"459","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3920)","author":"Jhala Ranjit","year":"2006","unstructured":"Ranjit Jhala and Kenneth L. McMillan. 2006. A Practical and Complete Approach to Predicate Refinement. In Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 3920), Holger Hermanns and Jens Palsberg (Eds.). Springer, 459-473. https:\/\/doi.org\/10.1007\/11691372_33 10.1007\/11691372_33"},{"key":"e_1_3_1_16_2","unstructured":"Adharsh Kamath Aditya Senthilnathan Saikat Chakraborty Pantazis Deligiannis Shuvendu K. Lahiri Akash Lal Aseem Rastogi Subhajit Roy and Rahul Sharma. 2023. Finding Inductive Loop Invariants using Large Language Models. https:\/\/doi.org\/10.48550\/arXiv.2311.07948 10.48550\/arXiv.2311.07948"},{"key":"e_1_3_1_17_2","first-page":"143","volume-title":"FMCAD","author":"Kragl Bernhard","year":"2021","unstructured":"Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In FMCAD. IEEE, 143-152. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_23 10.34727\/2021\/isbn.978-3-85448-046-4_23"},{"key":"e_1_3_1_18_2","first-page":"748","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017","author":"Lange Julien","year":"2017","unstructured":"Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2017. Fencing off go: liveness and safety for channel-based programming. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 748-761. https:\/\/doi.org\/10.1145\/3009837.3009847 10.1145\/3009837.3009847"},{"key":"e_1_3_1_19_2","first-page":"1137","volume-title":"Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018","author":"Lange Julien","year":"2018","unstructured":"Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A static verification framework for message passing in Go using behavioural types. In Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman (Eds.). ACM, 1137-1148. https:\/\/doi.org\/10.1145\/3180155.3180157 10.1145\/3180155.3180157"},{"key":"e_1_3_1_20_2","first-page":"348","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 6355)","author":"Rustan K.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 6355), Edmund M. Clarke and Andrei Voronkov (Eds.). Springer, 348-370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20 10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_21_2","first-page":"115","volume-title":"Engineering Trustworthy Software Systems - Third International School, SETSS 2017, Chongqing, China, April 17-22, 2017, Tutorial Lectures (Lecture Notes in Computer Science, Vol. 11174)","author":"Rustan K.","year":"2017","unstructured":"K. Rustan M. Leino. 2017. Modeling Concurrency in Dafny. In Engineering Trustworthy Software Systems - Third International School, SETSS 2017, Chongqing, China, April 17-22, 2017, Tutorial Lectures (Lecture Notes in Computer Science, Vol. 11174), Jonathan P. Bowen, Zhiming Liu, and Zili Zhang (Eds.). Springer, 115-142. https:\/\/doi.org\/10.1007\/978-3-030-02928-9_4 10.1007\/978-3-030-02928-9_4"},{"key":"e_1_3_1_22_2","first-page":"888","volume-title":"ASPLOS \u201822: 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, 28 February 2022 - 4 March 2022","author":"Liu Ziheng","year":"2022","unstructured":"Ziheng Liu, Shihao Xia, Yu Liang, Linhai Song, and Hong Hu. 2022. Who Goes First? Detecting Go Concurrency Bugs via Message Reordering. In ASPLOS \u201822: 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, 28 February 2022 - 4 March 2022. ACM, 888-902. https:\/\/doi.org\/10.1145\/3503222.3507753 10.1145\/3503222.3507753"},{"key":"e_1_3_1_23_2","first-page":"616","volume-title":"ASPLOS \u201821: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Virtual Event, USA, April 19-23, 2021","author":"Liu Ziheng","year":"2021","unstructured":"Ziheng Liu, Shuofei Zhu, Boqin Qin, Hao Chen, and Linhai Song. 2021. Automatically detecting and fixing concurrency bugs in go software systems. In ASPLOS \u201821: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Virtual Event, USA, April 19-23, 2021, Tim Sherwood, Emery D. Berger, and Christos Kozyrakis (Eds.). ACM, 616-629. https:\/\/doi.org\/10.1145\/3445814.3446756 10.1145\/3445814.3446756"},{"key":"e_1_3_1_24_2","first-page":"1","volume-title":"Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2725)","author":"McMillan Kenneth L.","year":"2003","unstructured":"Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (Lecture Notes in Computer Science, Vol. 2725), Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Springer, 1-13. https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1 10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_25_2","first-page":"284","volume-title":"Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11002)","author":"Midtgaard Jan","year":"2018","unstructured":"Jan Midtgaard, Flemming Nielson, and Hanne Riis Nielson. 2018. Process-Local Static Analysis of Synchronous Processes. In Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 11002), Andreas Podelski (Ed.). Springer, 284-305. https:\/\/doi.org\/10.1007\/978-3-319-99725-4_18 10.1007\/978-3-319-99725-4_18"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_3_1_27_2","first-page":"41","volume-title":"Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings (Lecture Notes in Computer Science, Vol. 9583)","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings (Lecture Notes in Computer Science, Vol. 9583), Barbara Jobstmann and K. Rustan M. Leino (Eds.). Springer, 41-62. https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2 10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_28_2","first-page":"174","volume-title":"Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016","author":"Ng Nicholas","year":"2016","unstructured":"Nicholas Ng and Nobuko Yoshida. 2016. Static deadlock detection for concurrent go by global session graph synthesis. In Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, Ayal Zaks and Manuel V. Hermenegildo (Eds.). ACM, 174-184. https:\/\/doi.org\/10.1145\/2892208.2892232 10.1145\/2892208.2892232"},{"key":"e_1_3_1_29_2","first-page":"42","volume-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016","author":"Padhi Saswat","year":"2016","unstructured":"Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-driven precondition inference with learned features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery D. Berger (Eds.). ACM, 42-56. https:\/\/doi.org\/10.1145\/2908080.2908099 10.1145\/2908080.2908099"},{"key":"e_1_3_1_30_2","first-page":"82","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 2031)","author":"Pnueli Amir","year":"2001","unstructured":"Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. 2001. Automatic Deductive Verification with Invisible Invariants. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 2031), Tiziana Margaria and Wang Yi (Eds.). Springer, 82-97. https:\/\/doi.org\/10.1007\/3-540-45319-9_7 10.1007\/3-540-45319-9_7"},{"key":"e_1_3_1_31_2","first-page":"411","volume-title":"IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2024, Edinburgh, United Kingdom, March 2-6, 2024","author":"Saioc Georgian-Vlad","year":"2024","unstructured":"Georgian-Vlad Saioc, Dmitriy Shirchenko, and Milind Chabbi. 2024. Unveiling and Vanquishing Goroutine Leaks in Enterprise Microservices: A Dynamic Analysis Approach. In IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2024, Edinburgh, United Kingdom, March 2-6, 2024, Tobias Grosser, Christophe Dubach, Michel Steuwer, Jingling Xue, Guilherme Ottoni, and ernando Magno Quint\u00e4o Pereira (Eds.). IEEE, 411-422. https:\/\/doi.org\/10.1109\/CGO57630.2024.10444835 10.1109\/CGO57630.2024.10444835"},{"key":"e_1_3_1_32_2","unstructured":"Georgian-Vlad Saioc and Milind Chabbi. 2022. LeakProf: Featherlight In-Production Goroutine Leak Detection. https:\/\/www.uber.com\/en-GB\/blog\/leakprof-featherlight-in-production-goroutine-leak-detection\/."},{"key":"e_1_3_1_33_2","unstructured":"Georgian-Vlad Saioc Julien Lange and Anders M\u00f8ller. 2024. VladSaioc\/oopsla-24-artifact: OOPSLA 24 Artifact. https:\/\/doi.org\/10.5281\/zenodo.13825844 10.5281\/zenodo.13825844"},{"key":"e_1_3_1_34_2","first-page":"53","volume-title":"Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 3148)","author":"Sankaranarayanan Sriram","year":"2004","unstructured":"Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Constraint-Based Linear-Relations Analysis. In Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 3148), Roberto Giacobazzi (Ed.). Springer, 53-68. https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7 10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_1_35_2","doi-asserted-by":"crossref","unstructured":"Kai Stadtm\u00fcller Martin Sulzmann and Peter Thiemann. 2016. Static Trace-Based Deadlock Analysis for Synchronous Mini-Go. In Programming Languages and Systems - 14th Asian Symposium APLAS 2016 Hanoi Vietnam November 21-23 2016 Proceedings (Lecture Notes in Computer Science Vol. 10017) Atsushi Igarashi (Ed.). 116-136. https:\/\/doi.org\/10.1007\/978-3-319-47958-3_7 10.1007\/978-3-319-47958-3_7","DOI":"10.1007\/978-3-319-47958-3_7"},{"key":"e_1_3_1_36_2","first-page":"22:1","volume-title":"Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018","author":"Sulzmann Martin","year":"2018","unstructured":"Martin Sulzmann and Kai Stadtm\u00fcller. 2018. Two-Phase Dynamic Analysis of Message-Passing Go Programs Based on Vector Clocks. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, David Sabel and Peter Thiemann (Eds.). ACM, 22:1-22:13. https:\/\/doi.org\/10.1145\/3236950.3236959 10.1145\/3236950.3236959"},{"key":"e_1_3_1_37_2","unstructured":"The Go Team. 2010. Share Memory by Communicating. https:\/\/go.dev\/doc\/effective_go."},{"key":"e_1_3_1_38_2","unstructured":"The Go Team. 2024. Go. https:\/\/go.dev\/."},{"key":"e_1_3_1_39_2","first-page":"32:1","volume-title":"37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022","author":"Veileborg Oskar Haarklou","year":"2022","unstructured":"Oskar Haarklou Veileborg, Georgian-Vlad Saioc, and Anders Moller. 2022. Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation. In 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022. ACM, 32:1-32:12. https:\/\/doi.org\/10.1145\/3551349.3561154 10.1145\/3551349.3561154"},{"key":"e_1_3_1_40_2","first-page":"367","volume-title":"Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 12759)","author":"Wolf Felix A.","year":"2021","unstructured":"Felix A. Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo\u00e4o Carlos Pereira, and Peter M\u00fcller. 2021. Gobra: Modular Specification and Verification of Go Programs. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 12759), Alexandra Silva and K. Rustan M. Leino (Eds.). Springer, 367-379. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_17 10.1007\/978-3-030-81685-8_17"},{"key":"e_1_3_1_41_2","first-page":"187","volume-title":"IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2021, Seoul, South Korea, February 27 - March 3, 2021","author":"Yuan Ting","year":"2021","unstructured":"Ting Yuan, Guangwei Li, Jie Lu, Chen Liu, Lian Li, and Jingling Xue. 2021. GoBench: A Benchmark Suite of Real-World Go Concurrency Bugs. In IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2021, Seoul, South Korea, February 27 - March 3, 2021, Jae W. Lee, Mary Lou Soffa, and Ayal Zaks (Eds.). IEEE, 187-199. https:\/\/doi.org\/10.1109\/CGO51591.2021.9370317 10.1109\/CGO51591.2021.9370317"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689784","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:10:40Z","timestamp":1770196240000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689784"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":40,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689784"],"URL":"https:\/\/doi.org\/10.1145\/3689784","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}