{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:29:55Z","timestamp":1784845795962,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,7,14]],"date-time":"2014-07-14T00:00:00Z","timestamp":1405296000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K040863\/1, EP\/H008373\/2, EP\/K032542\/1"],"award-info":[{"award-number":["EP\/K040863\/1, EP\/H008373\/2, EP\/K032542\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,7,14]]},"DOI":"10.1145\/2603088.2603091","type":"proceedings-article","created":{"date-parts":[[2014,7,28]],"date-time":"2014-07-28T13:21:45Z","timestamp":1406553705000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["A decision procedure for satisfiability in separation logic with inductive predicates"],"prefix":"10.1145","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[{"name":"University College London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[{"name":"University College London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juan A. Navarro","family":"P\u00e9rez","sequence":"additional","affiliation":[{"name":"University College London"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[{"name":"Middlesex University London"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/github.com\/ngorogiannis\/cyclist\/releases\/tag\/CSL-LICS14","author":"Satisfiability","unstructured":"Satisfiability checker for separation logic with inductive definitions. https:\/\/github.com\/ngorogiannis\/cyclist\/releases\/tag\/CSL-LICS14 . Satisfiability checker for separation logic with inductive definitions. https:\/\/github.com\/ngorogiannis\/cyclist\/releases\/tag\/CSL-LICS14."},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"411","volume-title":"FoSSaCS'14","author":"Antonopoulos T.","year":"2014","unstructured":"T. Antonopoulos , N. Gorogiannis , C. Haase , M. Kanovich , and J. Ouaknine . Foundations for decision problems in separation logic with general inductive predicates . In FoSSaCS'14 , volume 8412 of LNCS , pages 411 -- 425 , 2014 . T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In FoSSaCS'14, volume 8412 of LNCS, pages 411--425, 2014."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","first-page":"178","volume-title":"CAV'07","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'07 , volume 4590 of LNCS , 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'07, volume 4590 of LNCS, pages 178--192, 2007."},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","first-page":"178","volume-title":"CAV'11","author":"Berdine J.","year":"2011","unstructured":"J. Berdine , B. Cook , and S. Ishtiaq . SLAyer: Memory safety for systems-level code . In CAV'11 , volume 6806 of LNCS , pages 178 -- 183 , 2011 . J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: Memory safety for systems-level code. In CAV'11, volume 6806 of LNCS, pages 178--183, 2011."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_3_2_1_7_1","first-page":"3","volume-title":"SMT'12","author":"Bj\u00f8rner N.","year":"2012","unstructured":"N. Bj\u00f8rner , K. McMillan , and A. Rybalchenko . Program verification as satisfiability modulo theories . In SMT'12 , pages 3 -- 11 , 2012 . N. Bj\u00f8rner, K. McMillan, and A. Rybalchenko. Program verification as satisfiability modulo theories. In SMT'12, pages 3--11, 2012."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_1_9_1","series-title":"LNCS","first-page":"87","volume-title":"SAS'07","author":"Brotherston J.","year":"2007","unstructured":"J. Brotherston . Formalised inductive reasoning in the logic of bunched implications . In SAS'07 , volume 4634 of LNCS , pages 87 -- 103 , 2007 . J. Brotherston. Formalised inductive reasoning in the logic of bunched implications. In SAS'07, volume 4634 of LNCS, pages 87--103, 2007."},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","first-page":"350","volume-title":"APLAS'12","author":"Brotherston J.","year":"2012","unstructured":"J. Brotherston , N. Gorogiannis , and R. L. Petersen . A generic cyclic theorem prover . In APLAS'12 , volume 7705 of LNCS , pages 350 -- 367 , 2012 . J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS'12, volume 7705 of LNCS, pages 350--367, 2012."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_2_1_13_1","series-title":"LNCS","first-page":"384","volume-title":"SAS'07","author":"Chang B.-Y. E.","year":"2007","unstructured":"B.-Y. E. Chang , X. Rival , and G. Necula . Shape analysis with structural invariant checkers . In SAS'07 , volume 4634 of LNCS , pages 384 -- 401 , 2007 . B.-Y. E. Chang, X. Rival, and G. Necula. Shape analysis with structural invariant checkers. In SAS'07, volume 4634 of LNCS, pages 384--401, 2007."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_3_2_1_15_1","series-title":"LNCS","first-page":"235","volume-title":"CONCUR'11","author":"Cook B.","year":"2011","unstructured":"B. Cook , C. Haase , J. Ouaknine , M. J. Parkinson , and J. Worrell . Tractable reasoning in a fragment of separation logic . In CONCUR'11 , volume 6901 of LNCS , pages 235 -- 249 , 2011 . B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR'11, volume 6901 of LNCS, pages 235--249, 2011."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/502807.502810"},{"key":"e_1_3_2_1_17_1","series-title":"LNCS","first-page":"386","volume-title":"FM'11","author":"Gherghina C.","year":"2011","unstructured":"C. Gherghina , C. David , S. Qin , and W.-N. Chin . Structured specifications for better verification of heap-manipulating programs . In FM'11 , volume 6664 of LNCS , pages 386 -- 401 , 2011 . C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured specifications for better verification of heap-manipulating programs. In FM'11, volume 6664 of LNCS, pages 386--401, 2011."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","first-page":"457","volume-title":"CAV'11","author":"Hoder K.","year":"2011","unstructured":"K. Hoder , N. Bj\u00f8rner , and L. de Moura . μZ-- an efficient engine for fixed points with constraints. In CAV'11 , volume 6806 of LNCS , pages 457 -- 462 , 2011 . K. Hoder, N. Bj\u00f8rner, and L. de Moura. μZ-- an efficient engine for fixed points with constraints. In CAV'11, volume 6806 of LNCS, pages 457--462, 2011."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"e_1_3_2_1_22_1","series-title":"LNCS","first-page":"90","volume-title":"APLAS'13","author":"Navarro P\u00e9rez J. A.","year":"2013","unstructured":"J. A. Navarro P\u00e9rez and A. Rybalchenko . Separation logic modulo theories . In APLAS'13 , volume 8301 of LNCS , pages 90 -- 106 , 2013 . J. A. Navarro P\u00e9rez and A. Rybalchenko. Separation logic modulo theories. In APLAS'13, volume 8301 of LNCS, pages 90--106, 2013."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80009-2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958054"},{"key":"e_1_3_2_1_25_1","volume-title":"CAV'14","author":"Piskac R.","year":"2014","unstructured":"R. Piskac , T. Wies , and D. Zufferey . Enabling automated reasoning about separation logic of trees with data . In CAV'14 , 2014 . To appear. R. Piskac, T. Wies, and D. Zufferey. Enabling automated reasoning about separation logic of trees with data. In CAV'14, 2014. To appear."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/28659.28685"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"event":{"name":"CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC","location":"Vienna Austria","acronym":"CSL-LICS '14","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2603088.2603091","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2603088.2603091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:33Z","timestamp":1750278153000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2603088.2603091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,14]]},"references-count":27,"alternative-id":["10.1145\/2603088.2603091","10.1145\/2603088"],"URL":"https:\/\/doi.org\/10.1145\/2603088.2603091","relation":{},"subject":[],"published":{"date-parts":[[2014,7,14]]},"assertion":[{"value":"2014-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}