{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:43Z","timestamp":1790927623372,"version":"4.1.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"a UKRI Future Leaders Fellowship","award":["MR\/V024299\/1"],"award-info":[{"award-number":["MR\/V024299\/1"]}]},{"DOI":"10.13039\/501100000266","name":"UK?s Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council (ERC) Consolidator Grant","award":["683289"],"award-info":[{"award-number":["683289"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>Incorrectness Logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs\u2014dual to Hoare Logic, which is used to compositionally prove their absence. Though IL was motivated in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in developing new analyses which can catch real bugs in big programs?<\/jats:p>\n          <jats:p>In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used analyzer which has proven useful in industrial engineering practice.<\/jats:p>","DOI":"10.1145\/3527325","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":57,"title":["Finding real bugs in big programs with incorrectness logic"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6220-7539","authenticated-orcid":false,"given":"Quang Loc","family":"Le","sequence":"first","affiliation":[{"name":"University College London, UK \/ Meta, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, UK \/ Meta, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8637-0712","authenticated-orcid":false,"given":"Jules","family":"Villard","sequence":"additional","affiliation":[{"name":"Meta, 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,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454076"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_8"},{"key":"e_1_2_1_3_1","volume-title":"Sys: A Static\/Symbolic Tool for Finding Good Bugs in Good (Browser) Code. In 29th USENIX Security Symposium (USENIX Security 20)","author":"Brown Fraser","year":"2020","unstructured":"Fraser Brown , Deian Stefan , and Dawson Engler . 2020 . Sys: A Static\/Symbolic Tool for Finding Good Bugs in Good (Browser) Code. In 29th USENIX Security Symposium (USENIX Security 20) . USENIX Association, 199\u2013216. isbn:978-1-939133-17-5 https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/brown Fraser Brown, Deian Stefan, and Dawson Engler. 2020. Sys: A Static\/Symbolic Tool for Finding Good Bugs in Good (Browser) Code. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, 199\u2013216. isbn:978-1-939133-17-5 https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/brown"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_19"},{"key":"e_1_2_1_7_1","volume-title":"Reverse Hoare Logic","author":"de Vries Edsko","unstructured":"Edsko de Vries and Vasileios Koutavas . 2011. Reverse Hoare Logic . In Software Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 155\u2013171. isbn:978-3-642-24690-6 Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods, Gilles Barthe, Alberto Pardo, and Gerardo Schneider (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 155\u2013171. isbn:978-3-642-24690-6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254087"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_11_1","unstructured":"Facebook. 2021. https:\/\/fbinfer.com\/  Facebook. 2021. https:\/\/fbinfer.com\/"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2015.7102580"},{"key":"e_1_2_1_16_1","volume-title":"FuzzGen: Automatic Fuzzer Generation. In 29th USENIX Security Symposium, USENIX Security 2020","author":"Ispoglou Kyriakos K.","year":"2020","unstructured":"Kyriakos K. Ispoglou , Daniel Austin , Vishwath Mohan , and Mathias Payer . 2020 . FuzzGen: Automatic Fuzzer Generation. In 29th USENIX Security Symposium, USENIX Security 2020 , August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 2271\u20132287. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/ispoglou Kyriakos K. Ispoglou, Daniel Austin, Vishwath Mohan, and Mathias Payer. 2020. FuzzGen: Automatic Fuzzer Generation. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 2271\u20132287. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/ispoglou"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_19_1","volume-title":"Shape Analysis via Second-Order Bi-Abduction","author":"Le Quang Loc","unstructured":"Quang Loc Le , Cristian Gherghina , Shengchao Qin , and Wei-Ngan Chin . 2014. Shape Analysis via Second-Order Bi-Abduction . In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham . 52\u201368. isbn:978-3-319-08867-9 Quang Loc Le, Cristian Gherghina, Shengchao Qin, and Wei-Ngan Chin. 2014. Shape Analysis via Second-Order Bi-Abduction. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 52\u201368. isbn:978-3-319-08867-9"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6342311"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_23_1","unstructured":"Peter W. O\u2019Hearn. 2015. https:\/\/mailing.openssl.dev.narkive.com\/2DbkkYzD\/openssl-org-3403-null-dereference-and-memory-leak-reports-for-openssl-1-0-1h-from-facebook-s-infer  Peter W. O\u2019Hearn. 2015. https:\/\/mailing.openssl.dev.narkive.com\/2DbkkYzD\/openssl-org-3403-null-dereference-and-memory-leak-reports-for-openssl-1-0-1h-from-facebook-s-infer"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_26_1","volume-title":"Theory and Practice of Mechanized Software Analysis. In Johns Hopkins APL Technical Digest","volume":"32","author":"Pendergrass J.A.","unstructured":"J.A. Pendergrass , S.C. Lee , and C.D. McConnell . 2013 . Theory and Practice of Mechanized Software Analysis. In Johns Hopkins APL Technical Digest , Volume 32 , Number 2. 499\u2013508. J.A. Pendergrass, S.C. Lee, and C.D. McConnell. 2013. Theory and Practice of Mechanized Software Analysis. In Johns Hopkins APL Technical Digest, Volume 32, Number 2. 499\u2013508."},{"key":"e_1_2_1_27_1","volume-title":"Quoc-Sang Phan, Jun Sun, and Shengchao Qin.","author":"Pham Long H.","year":"2019","unstructured":"Long H. Pham , Quang Loc Le , Quoc-Sang Phan, Jun Sun, and Shengchao Qin. 2019 . Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation. In Automated Technology for Verification and Analysis, Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza (Eds.). Springer International Publishing , Cham. 209\u2013227. isbn:978-3-030-31784-3 Long H. Pham, Quang Loc Le, Quoc-Sang Phan, Jun Sun, and Shengchao Qin. 2019. Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation. In Automated Technology for Verification and Analysis, Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza (Eds.). Springer International Publishing, Cham. 209\u2013227. isbn:978-3-030-31784-3"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_2_1_30_1","volume-title":"Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In 24th USENIX Security Symposium (USENIX Security 15)","author":"David","unstructured":"David A. Ramos and Dawson Engler. 2015 . Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In 24th USENIX Security Symposium (USENIX Security 15) . USENIX Association, Washington, D.C.. 49\u201364. isbn:978-1-939133-11-3 https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/ramos David A. Ramos and Dawson Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In 24th USENIX Security Symposium (USENIX Security 15). USENIX Association, Washington, D.C.. 49\u201364. isbn:978-1-939133-11-3 https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/ramos"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":31,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527325"],"URL":"https:\/\/doi.org\/10.1145\/3527325","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}