{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T03:25:17Z","timestamp":1778037917203,"version":"3.51.4"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0204242"],"award-info":[{"award-number":["CCR-0204242"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2009,4]]},"abstract":"<jats:p>We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a form of dynamic partitioning, where we track the transfer of ownership of portions of heap storage between program components. It also enables us to enforce separation in the presence of mutable data structures with embedded addresses that may be aliased.<\/jats:p>","DOI":"10.1145\/1498926.1498929","type":"journal-article","created":{"date-parts":[[2009,4,15]],"date-time":"2009-04-15T13:37:07Z","timestamp":1239802627000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Separation and information hiding"],"prefix":"10.1145","volume":"31","author":[{"given":"Peter W.","family":"O'Hearn","sequence":"first","affiliation":[{"name":"Queen Mary, University of London"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John C.","family":"Reynolds","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,4,21]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS). 33--44","author":"Ahmed A."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_17"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.47"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS).","author":"Birkedal L."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Bornat R. 2000. Proving pointer programs in Hoare logic. Mathematics of Program Construction. Bornat R. 2000. Proving pointer programs in Hoare logic. Mathematics of Program Construction.","DOI":"10.1007\/10722010_8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_10_1","volume-title":"2002. The Origin of Concurrent Programming","author":"Brinch Hansen P."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680008"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504300"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Hoare C. A. R. 1972b. Towards a theory of parallel programming. In Operating Systems Techniques Hoare and Perrot Eds. Academic Press. Hoare C. A. R. 1972b. Towards a theory of parallel programming. In Operating Systems Techniques Hoare and Perrot Eds. Academic Press.","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_21_1","unstructured":"Kernighan B. and Ritchie D. 1988. The C Programming Language. Prentice Hall. Second edition. Kernighan B. and Ritchie D. 1988. The C Programming Language. Prentice Hall. Second edition."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs.","author":"Krishnaswami N."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP).","author":"Leino K."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_28_1","volume-title":"Foundations of Component-Based Systems","author":"M\u00fcller P."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0020-5"},{"key":"e_1_2_1_31_1","unstructured":"Naumann D. A. and Barnett M. 2004a. Friends need a bit more: Maintaining invariants over shared state. In Mathematics of Program Construction. Naumann D. A. and Barnett M. 2004a. Friends need a bit more: Maintaining invariants over shared state. In Mathematics of Program Construction."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021868"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19","author":"O'Hearn P."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_2_1_37_1","volume-title":"Class invariants: the end of the road&quest","author":"Parkinson M."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.52"},{"key":"e_1_2_1_40_1","first-page":"339","article-title":"Information distribution aspects of design methodology","volume":"1","author":"Parnas D.","year":"1972","journal-title":"Proceedings of International Federation for Information Processing (IFIP)"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 17th European Symposium on Programming (ESOP).","author":"Peterson R."},{"key":"e_1_2_1_43_1","unstructured":"Plotkin G. 1983. Pisa notes (on domain theory). Plotkin G. 1983. Pisa notes (on domain theory)."},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of International Federation for Information Processing (IFIP).","author":"Reynolds J. C.","year":"1983"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/20.2.151"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1498926.1498929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1498926.1498929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:38:39Z","timestamp":1750253919000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1498926.1498929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["10.1145\/1498926.1498929"],"URL":"https:\/\/doi.org\/10.1145\/1498926.1498929","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,4]]},"assertion":[{"value":"2008-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}