{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T03:35:27Z","timestamp":1791516927994,"version":"4.3.4"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T00:00:00Z","timestamp":1548633600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2019,1,28]]},"abstract":"<jats:p>Separation logic is a key development in formal reasoning about programs, opening up new lines of attack on longstanding problems.<\/jats:p>","DOI":"10.1145\/3211968","type":"journal-article","created":{"date-parts":[[2019,1,29]],"date-time":"2019-01-29T13:16:22Z","timestamp":1548767782000},"page":"86-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":86,"title":["Separation logic"],"prefix":"10.1145","volume":"62","author":[{"given":"Peter","family":"O'Hearn","sequence":"first","affiliation":[{"name":"Facebook and University College London, U.K"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,28]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_3_1","first-page":"183","article-title":"SLAyer: Memory safety for systems-level code","volume":"178","author":"Berdine J.","year":"2011","journal-title":"Proceedings of CAV"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2831143.2831157"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_2_6_1","first-page":"102","article-title":"Proving pointer programs in Hoare logic","volume":"1837","author":"Bornat R","year":"2000","journal-title":"LNCS MPC"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_2_10_1","first-page":"1","article-title":"Some techniques for proving correctness of programs which alter data structures","volume":"7","author":"Burstall R.M","year":"1972","journal-title":"Machine Intelligence"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_16_1","volume-title":"Cooperating sequential processes. Programming Languages","author":"Dijkstra E.W.","year":"1968"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_18_1","first-page":"528","article-title":"Concurrent abstract predicates","volume":"504","author":"Dinsdale-Young T.","year":"2010","journal-title":"Proceedings of ECOOP"},{"key":"e_1_2_2_19_1","first-page":"215","article-title":"Abstraction and refinement for local reasoning","volume":"199","author":"Dinsdale-Young T.","year":"2010","journal-title":"Proceedings of VSTTE"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_23_1","volume-title":"Towards a theory of parallel programming. Operating Systems Techniques","author":"Hoare C.A.R.","year":"1972"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2011.04.005"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of IFIP Congress","author":"Jones C.B.","year":"1983"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_32_1","first-page":"19","article-title":"Local reasoning about programs that alter data structures","volume":"1","author":"O'Hearn P.W.","year":"2001","journal-title":"Proceedings of CSL"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.52"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.01.006"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_2_37_1","volume-title":"Cornerstones of Computing","author":"Reynolds J,C","year":"2000"},{"key":"e_1_2_2_38_1","first-page":"74","article-title":"A logic for shared mutable data structures","volume":"55","author":"Reynolds J.C.","year":"2002","journal-title":"LICS"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_40_1","first-page":"69","article-title":"Checking a large routine. Report of a Conference on High-Speed Automatic Calculating Machines. Univ. Math. Lab., Cambridge","volume":"67","author":"Turing A.M","year":"1949","journal-title":"U.K."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"},{"key":"e_1_2_2_44_1","first-page":"416","article-title":"A semantic basis for local reasoning","volume":"402","author":"Yang H.","year":"2002","journal-title":"Proceedings of FoSSaCS"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3211968","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3211968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:14Z","timestamp":1750210754000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3211968"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,28]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,1,28]]}},"alternative-id":["10.1145\/3211968"],"URL":"https:\/\/doi.org\/10.1145\/3211968","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,28]]},"assertion":[{"value":"2019-01-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}