{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:14:08Z","timestamp":1791299648673,"version":"4.1.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"UKRI Future Leaders Fellowship","award":["MR\/V024299\/1"],"award-info":[{"award-number":["MR\/V024299\/1"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop\n            <jats:italic>concurrent incorrectness separation logic<\/jats:italic>\n            (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the\n            <jats:italic>soundness<\/jats:italic>\n            of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.\n          <\/jats:p>","DOI":"10.1145\/3498695","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Concurrent incorrectness separation logic"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9691-1348","authenticated-orcid":false,"given":"Josh","family":"Berdine","sequence":"additional","affiliation":[{"name":"Meta, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8730-5496","authenticated-orcid":false,"given":"Peter W.","family":"O'Hearn","sequence":"additional","affiliation":[{"name":"Meta, UK \/ University College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276514"},{"key":"e_1_2_2_3_1","article-title":"Concurrent separation logic","volume":"3","author":"Brookes Stephen","year":"2016","unstructured":"Stephen Brookes and Peter W. O'Hearn . 2016 . Concurrent separation logic . SIGLOG News 3 , 3 ( 2016 ), 47-65. https: \/\/dl.acm.org\/citation.cfm?id= 2984457 Stephen Brookes and Peter W. O'Hearn. 2016. Concurrent separation logic. SIGLOG News 3, 3 ( 2016 ), 47-65. https: \/\/dl.acm.org\/citation.cfm?id= 2984457","journal-title":"SIGLOG News"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678572"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1736020.1736040"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_7_1","first-page":"504","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010-Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young , Mike Dodds , Philippa Gardner , Matthew J. Parkinson , and Viktor Vafeiadis . 2010 . Concurrent Abstract Predicates. In ECOOP 2010-Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 504 - 528 . Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010-Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504-528."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290370"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250765"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion.2019.00042"},{"key":"e_1_2_2_14_1","volume-title":"Communicating State Transition Systems for Fine-Grained Concurrent Resources","author":"Nanevski Aleksandar","unstructured":"Aleksandar Nanevski , Ruy Ley-Wild , Ilya Sergey , and Germ\u00e1n Andr\u00e9s Delbianco . 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources . In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 290-310. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germ\u00e1n Andr\u00e9s Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 290-310."},{"key":"e_1_2_2_15_1","first-page":"49","volume-title":"Concurrency and Local Reasoning. In CONCUR 2004-Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg","author":"O'Hearn Peter W.","year":"2004","unstructured":"Peter W. O'Hearn . 2004 . Resources , Concurrency and Local Reasoning. In CONCUR 2004-Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 49 - 67 . Peter W. O'Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004-Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 49-67."},{"key":"e_1_2_2_16_1","volume-title":"Experience Developing and Deploying Concurrency Analysis at Facebook","author":"O'Hearn Peter W.","unstructured":"Peter W. O'Hearn . 2018. Experience Developing and Deploying Concurrency Analysis at Facebook . In Static Analysis, Andreas Podelski (Ed.). Springer International Publishing , Cham , 56-70. Peter W. O'Hearn. 2018. Experience Developing and Deploying Concurrency Analysis at Facebook. In Static Analysis, Andreas Podelski (Ed.). Springer International Publishing, Cham, 56-70."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_20_1","volume-title":"Verified Software: Theories, Tools, Experiments, Gary T. Leavens, Peter O'Hearn, and Sriram K","author":"Parkinson Matthew","unstructured":"Matthew Parkinson . 2010. The Next 700 Separation Logics . In Verified Software: Theories, Tools, Experiments, Gary T. Leavens, Peter O'Hearn, and Sriram K . Rajamani (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 169-182. Matthew Parkinson. 2010. The Next 700 Separation Logics. In Verified Software: Theories, Tools, Experiments, Gary T. Leavens, Peter O'Hearn, and Sriram K. Rajamani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 169-182."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_2_22_1","volume-title":"Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic","author":"Raad Azalea","unstructured":"Azalea Raad , Josh Berdine , Hoang-Hai Dang , Derek Dreyer , Peter O'Hearn , and Jules Villard . 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic . In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing , Cham , 225-252. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 225-252."},{"key":"e_1_2_2_23_1","unstructured":"Azalea Raad Josh Berdine Derek Dreyer and Peter O'Hearn. 2022. Technical Appendix. https:\/\/www.soundandcomplete. org\/papers\/POPL2022\/CISL\/appendix.pdf  Azalea Raad Josh Berdine Derek Dreyer and Peter O'Hearn. 2022. Technical Appendix. https:\/\/www.soundandcomplete. org\/papers\/POPL2022\/CISL\/appendix.pdf"},{"key":"e_1_2_2_24_1","volume-title":"CoLoSL: Concurrent Local Subjective Logic","author":"Raad Azalea","unstructured":"Azalea Raad , Jules Villard , and Philippa Gardner . 2015. CoLoSL: Concurrent Local Subjective Logic . In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 710-735. Azalea Raad, Jules Villard, and Philippa Gardner. 2015. CoLoSL: Concurrent Local Subjective Logic. In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 710-735."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1791194.1791203"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498695","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":27,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498695"],"URL":"https:\/\/doi.org\/10.1145\/3498695","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}