{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:39Z","timestamp":1772163999380,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,1,26]],"date-time":"2011-01-26T00:00:00Z","timestamp":1296000000000},"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,1,26]]},"DOI":"10.1145\/1926385.1926455","type":"proceedings-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T09:58:22Z","timestamp":1295863102000},"page":"611-622","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Decidable logics combining heap structures and data"],"prefix":"10.1145","author":[{"given":"P.","family":"Madhusudan","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]},{"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[{"name":"LIAFA, CNRS and University of Paris Diderot, Paris, IL, USA"}]},{"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2011,1,26]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_13"},{"key":"e_1_3_2_2_6_1","volume-title":"The Classical Decision Problem","author":"B\u00f6rger E.","year":"2001","unstructured":"E. B\u00f6rger , E. Gr\u00e4del , and Y. Gurevich . The Classical Decision Problem . Springer , 2001 . E. B\u00f6rger, E. Gr\u00e4del, and Y. Gurevich. The Classical Decision Problem. Springer, 2001."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_13"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_35"},{"key":"e_1_3_2_2_9_1","series-title":"LNCS","first-page":"337","volume-title":"TACAS'08","author":"de Moura L. M.","year":"2008","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: An efficient SMT solver . In TACAS'08 , volume 4963 of LNCS , pages 337 -- 340 . Springer , 2008 . L. M. de Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In TACAS'08, volume 4963 of LNCS, pages 337--340. Springer, 2008."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/267871.267874"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_2_13_1","volume-title":"Department of Computer Science","author":"Klarlund N.","year":"2001","unstructured":"N. Klarlund and A. M\u00f8ller . MONA. BRICS , Department of Computer Science , Aarhus University , January 2001 . Available from http:\/\/www.brics.dk\/mona\/. N. Klarlund and A. M\u00f8ller. MONA. BRICS, Department of Computer Science, Aarhus University, January 2001. Available from http:\/\/www.brics.dk\/mona\/."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158628"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_2_17_1","series-title":"LNCS","first-page":"280","volume-title":"SAS'00","author":"Lev-Ami T.","year":"2000","unstructured":"T. Lev-Ami and S. Sagiv . Tvla: A system for implementing static analyses . In SAS'00 , volume 1824 of LNCS , pages 280 -- 301 . Springer , 2000 . T. Lev-Ami and S. Sagiv. Tvla: A system for implementing static analyses. In SAS'00, volume 1824 of LNCS, pages 280--301. Springer, 2000."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_41"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_47"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567073"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_2_23_1","series-title":"LNCS","first-page":"106","volume-title":"VMCAI'07","author":"Rakamari\u0107 Z.","year":"2007","unstructured":"Z. Rakamari\u0107 , J. D. Bingham , and A. J. Hu . An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures . In VMCAI'07 , volume 4349 of LNCS , pages 106 -- 121 . Springer , 2007 . Z. Rakamari\u0107, J. D. Bingham, and A. J. Hu. An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In VMCAI'07, volume 4349 of LNCS, pages 106--121. Springer, 2007."},{"key":"e_1_3_2_2_24_1","series-title":"LNCS","first-page":"237","volume-title":"ATVA'07","author":"Rakamari\u0107 Z.","year":"2007","unstructured":"Z. Rakamari\u0107 , R. Bruttomesso , A. J. Hu , and A. Cimatti . Verifying heap-manipulating programs in an SMT framework . In ATVA'07 , volume 4762 of LNCS , pages 237 -- 252 . Springer , 2007 . Z. Rakamari\u0107, R. Bruttomesso, A. J. Hu, and A. Cimatti. Verifying heap-manipulating programs in an SMT framework. In ATVA'07, volume 4762 of LNCS, pages 237--252. Springer, 2007."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.7"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_2_27_1","series-title":"LNCS","first-page":"530","volume-title":"TACAS'04","author":"Yorsh G.","year":"2004","unstructured":"G. Yorsh , T. W. Reps , and S. Sagiv . Symbolically computing most-precise abstract operations for shape analysis . In TACAS'04 , volume 2988 of LNCS , pages 530 -- 545 . Springer , 2004 . G. Yorsh, T. W. Reps, and S. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS'04, volume 2988 of LNCS, pages 530--545. Springer, 2004."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_7"}],"event":{"name":"POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Austin Texas USA","acronym":"POPL '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926455","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1926385.1926455","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:52:46Z","timestamp":1750229566000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926455"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,26]]},"references-count":27,"alternative-id":["10.1145\/1926385.1926455","10.1145\/1926385"],"URL":"https:\/\/doi.org\/10.1145\/1926385.1926455","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1925844.1926455","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,1,26]]},"assertion":[{"value":"2011-01-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}