{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T02:43:29Z","timestamp":1790477009985,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,17]],"date-time":"2010-01-17T00:00:00Z","timestamp":1263686400000},"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":[],"published-print":{"date-parts":[[2010,1,17]]},"DOI":"10.1145\/1706299.1706331","type":"proceedings-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T15:15:04Z","timestamp":1263914104000},"page":"261-274","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Structuring the verification of heap-manipulating programs"],"prefix":"10.1145","author":[{"given":"Aleksandar","family":"Nanevski","sequence":"first","affiliation":[{"name":"IMDEA Software, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josh","family":"Berdine","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tactics for separation logic.","author":"Appel A. W.","year":"2006","unstructured":"A. W. Appel . Tactics for separation logic. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf, 2006 . A. W. Appel. Tactics for separation logic. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf, 2006."},{"key":"e_1_3_2_1_2_1","first-page":"365","volume-title":"FoSSaCS'08","author":"Barras B.","unstructured":"B. Barras and B. Bernardo . The implicit calculus of constructions as a programming language with dependent types . In FoSSaCS'08 , pages 365 -- 379 . B. Barras and B. Bernardo. The implicit calculus of constructions as a programming language with dependent types. In FoSSaCS'08, pages 365--379."},{"key":"e_1_3_2_1_3_1","volume-title":"Design and results of the 4th annual satisfiability modulo theories competition (SMT-COMP","author":"Barrett C.","year":"2008","unstructured":"C. Barrett , M. Deters , A. Oliveras , and A. Stump . Design and results of the 4th annual satisfiability modulo theories competition (SMT-COMP 2008 ). To appear. C. Barrett, M. Deters, A. Oliveras, and A. Stump. Design and results of the 4th annual satisfiability modulo theories competition (SMT-COMP 2008). To appear."},{"key":"e_1_3_2_1_5_1","first-page":"178","volume-title":"CAV'07","author":"Berdine J.","unstructured":"J. Berdine , C. Calcagno , B. Cook , D. Distefano , P. W. O'Hearn , T. Wies , and H. Yang . Shape analysis for composite data structures . In CAV'07 , pages 178 -- 192 . J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV'07, pages 178--192."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_2_1_7_1","volume-title":"Relational parametricity and separation logic. Logical Methods in Computer Science, 4(2:6):1--27","author":"Birkedal L.","year":"2008","unstructured":"L. Birkedal and H. Yang . Relational parametricity and separation logic. Logical Methods in Computer Science, 4(2:6):1--27 , 2008 . L. Birkedal and H. Yang. Relational parametricity and separation logic. Logical Methods in Computer Science, 4(2:6):1--27, 2008."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375603"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.707"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481874"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"issue":"3","key":"e_1_3_2_1_17_1","first-page":"135","article-title":"A certified verifier for a fragment of separation logic","volume":"25","author":"Marty N.","year":"2008","unstructured":"N. Marty and R. Affeldt . A certified verifier for a fragment of separation logic . Computer Software , 25 ( 3 ): 135 -- 147 , 2008 . N. Marty and R. Affeldt. A certified verifier for a fragment of separation logic. Computer Software, 25(3):135--147, 2008.","journal-title":"Computer Software"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_24"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.009"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"e_1_3_2_1_25_1","first-page":"1","volume-title":"CSL'01","author":"O'Hearn P.","unstructured":"P. O'Hearn , J. Reynolds , and H. Yang . Local reasoning about programs that alter data structures . In CSL'01 , pages 1 -- 19 . P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL'01, pages 1--19."},{"key":"e_1_3_2_1_26_1","first-page":"55","volume-title":"LICS'02","author":"Reynolds J. C.","unstructured":"J. C. Reynolds . Separation logic : A logic for shared mutable data structures . In LICS'02 , pages 55 -- 74 . J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02, pages 55--74."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542514"}],"event":{"name":"POPL '10: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Madrid Spain","acronym":"POPL '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706331","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1706299.1706331","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:26:19Z","timestamp":1750263979000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1706299.1706331"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,17]]},"references-count":25,"alternative-id":["10.1145\/1706299.1706331","10.1145\/1706299"],"URL":"https:\/\/doi.org\/10.1145\/1706299.1706331","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1707801.1706331","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,17]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}