{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:07Z","timestamp":1772164027437,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,6,4]],"date-time":"2011-06-04T00:00:00Z","timestamp":1307145600000},"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":[[2011,6,4]]},"DOI":"10.1145\/1993498.1993563","type":"proceedings-article","created":{"date-parts":[[2011,6,6]],"date-time":"2011-06-06T07:53:52Z","timestamp":1307346832000},"page":"556-566","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Separation logic + superposition calculus = heap theorem prover"],"prefix":"10.1145","author":[{"given":"Juan Antonio","family":"Navarro P\u00e9rez","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,6,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_1_2_1","first-page":"298","volume-title":"CAV","author":"Barrett C.","year":"2007","unstructured":"C. Barrett and C. Tinelli . CVC3 . In CAV , pages 298 -- 302 , 2007 . C. Barrett and C. Tinelli. CVC3. In CAV, pages 298--302, 2007."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"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","first-page":"178","volume-title":"CAV","author":"Berdine J.","year":"2007","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 , pages 178 -- 192 , 2007 . 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, pages 178--192, 2007."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763055"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_3_2_1_11_1","first-page":"233","volume-title":"SAS","author":"Calcagno C.","year":"2007","unstructured":"C. Calcagno , M. Parkinson , and V. Vafeiadis . SmallfootRG . In SAS , pages 233 -- 238 , 2007 . C. Calcagno, M. Parkinson, and V. Vafeiadis. SmallfootRG. In SAS, pages 233--238, 2007."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328469"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_15_1","volume-title":"FORMATS","author":"de Moura L. M.","year":"2009","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Tapas theory combinations and practical applications . In FORMATS , 2009 . L. M. de Moura and N. Bj\u00f8rner. Tapas theory combinations and practical applications. In FORMATS, 2009."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_3_2_1_19_1","volume-title":"Computer Science Laboratory","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. D. Moura . The Yices SMT solver. Technical report , Computer Science Laboratory , SRI International , 2006 . B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International, 2006."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277748"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_24_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic (CSL'07)","author":"Korovin K.","year":"2007","unstructured":"K. Korovin and A. Voronkov . Integrating linear arithmetic into superposition calculus . In Computer Science Logic (CSL'07) , volume 4646 of Lecture Notes in Computer Science , pages 223 -- 237 . Springer , 2007 . K. Korovin and A. Voronkov. Integrating linear arithmetic into superposition calculus. In Computer Science Logic (CSL'07), volume 4646 of Lecture Notes in Computer Science, pages 223--237. Springer, 2007."},{"issue":"3","key":"e_1_3_2_1_25_1","first-page":"135","article-title":"A certified verifier for a fragment of separation logic","volume":"25","author":"Marti N.","year":"2008","unstructured":"N. Marti and R. Affeldt . A certified verifier for a fragment of separation logic . Computer Software , 25 ( 3 ): 135 -- 147 , 2008 . N. Marti 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_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787543"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787545"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_19"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706330"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_1"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_23"},{"key":"e_1_3_2_1_37_1","volume-title":"SPACE workshop","author":"Yang H.","year":"2001","unstructured":"H. Yang . An example of local reasoning in bi pointer logic: the schorr-waite graph marking algorithm . In SPACE workshop , 2001 . H. Yang. An example of local reasoning in bi pointer logic: the schorr-waite graph marking algorithm. In SPACE workshop, 2001."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"event":{"name":"PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"San Jose California USA","acronym":"PLDI '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1993498.1993563","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1993498.1993563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:00:04Z","timestamp":1750230004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1993498.1993563"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,4]]},"references-count":37,"alternative-id":["10.1145\/1993498.1993563","10.1145\/1993498"],"URL":"https:\/\/doi.org\/10.1145\/1993498.1993563","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1993316.1993563","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,6,4]]},"assertion":[{"value":"2011-06-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}