{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:49Z","timestamp":1772164069671,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC","award":["EP\/K040049\/1, EP\/J002224\/1"],"award-info":[{"award-number":["EP\/K040049\/1, EP\/J002224\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837621","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"84-96","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Model checking for symbolic-heap separation logic with inductive predicates"],"prefix":"10.1145","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[{"name":"University College London, UK"}]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[{"name":"Middlesex University, UK"}]},{"given":"Max","family":"Kanovich","sequence":"additional","affiliation":[{"name":"University College London, UK \/ National Research University Higher School of Economics, Russia"}]},{"given":"Reuben","family":"Rowe","sequence":"additional","affiliation":[{"name":"University College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"C YCLIST : software distribution. https:\/\/github.com\/ngorogiannis\/cyclist\/.  C YCLIST : software distribution. https:\/\/github.com\/ngorogiannis\/cyclist\/."},{"key":"e_1_3_2_1_2_1","unstructured":"Project Archer GDB development branch. https:\/\/sourceware.org\/gdb\/wiki\/ProjectArcher.  Project Archer GDB development branch. https:\/\/sourceware.org\/gdb\/wiki\/ProjectArcher."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. FoSSaCS-17","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 Proc. FoSSaCS-17 . Springer , 2014 . T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Proc. FoSSaCS-17. Springer, 2014."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. CAV-23","author":"Berdine J.","year":"2011","unstructured":"J. Berdine , B. Cook , and S. Ishtiaq . SLAyer: memory safety for systems-level code . In Proc. CAV-23 . Springer , 2011 . J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: memory safety for systems-level code. In Proc. CAV-23. Springer, 2011."},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. 1st BOOGIE","author":"Botincan M.","year":"2011","unstructured":"M. Botincan , D. Distefano , M. Dodds , R. Grigore , D. Naudziuniene , and M. J. Parkinson . coreStar: The core of jStar . In Proc. 1st BOOGIE , 2011 . M. Botincan, D. Distefano, M. Dodds, R. Grigore, D. Naudziuniene, and M. J. Parkinson. coreStar: The core of jStar. In Proc. 1st BOOGIE, 2011."},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. SAS-14","author":"Brotherston J.","year":"2007","unstructured":"J. Brotherston . Formalised inductive reasoning in the logic of bunched implications . In Proc. SAS-14 . Springer , 2007 . J. Brotherston. Formalised inductive reasoning in the logic of bunched implications. In Proc. SAS-14. Springer, 2007."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. SAS-21","author":"Brotherston J.","year":"2014","unstructured":"J. Brotherston and N. Gorogiannis . Cyclic abduction of inductively defined safety and termination preconditions . In Proc. SAS-21 . Springer , 2014 . J. Brotherston and N. Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. In Proc. SAS-21. Springer, 2014."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_20"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. APLAS-10","author":"Brotherston J.","year":"2012","unstructured":"J. Brotherston , N. Gorogiannis , and R. L. Petersen . A generic cyclic theorem prover . In Proc. APLAS-10 , LNCS. Springer , 2012 . J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In Proc. APLAS-10, LNCS. Springer, 2012."},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. NFM-3","author":"Calcagno C.","year":"2011","unstructured":"C. Calcagno and D. Distefano . Infer: An automatic program verifier for memory safety of C programs . In Proc. NFM-3 . Springer , 2011 . C. Calcagno and D. Distefano. Infer: An automatic program verifier for memory safety of C programs. In Proc. NFM-3. Springer, 2011."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737984"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. CAV-23","author":"Dudka K.","year":"2011","unstructured":"K. Dudka , P. Peringer , and T. Vojnar . Predator: A practical tool for checking manipulation of dynamic data structures using separation logic . In Proc. CAV-23 . Springer , 2011 . K. Dudka, P. Peringer, and T. Vojnar. Predator: A practical tool for checking manipulation of dynamic data structures using separation logic. In Proc. CAV-23. Springer, 2011."},{"key":"e_1_3_2_1_20_1","first-page":"130","author":"Frick M.","year":"2004","unstructured":"M. Frick and M. Grohe . The complexity of first-order and monadic second-order logic revisited. Annals of Pure and Applied Logic , 130 , 2004 . M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited. Annals of Pure and Applied Logic, 130, 2004.","journal-title":"Annals of Pure and Applied Logic"},{"key":"e_1_3_2_1_21_1","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"Garey M. R.","year":"1979","unstructured":"M. R. Garey and D. S. Johnson . Computers and Intractability: A Guide to the Theory of NP-Completeness . W. H. Freeman , 1979 . M. R. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. NFM-3","author":"Jacobs B.","year":"2011","unstructured":"B. Jacobs , J. Smans , P. Philippaerts , F. Vogels , W. Penninckx , and F. Piessens . Verifast: A powerful, sound, predictable, fast verifier for C and Java . In Proc. NFM-3 . Springer , 2011 . B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In Proc. NFM-3. Springer, 2011."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"e_1_3_2_1_26_1","volume-title":"Proc. VMCAI-9","author":"Nguyen H. H.","year":"2008","unstructured":"H. H. Nguyen , V. Kuncak , and W.-N. Chin . Runtime checking for separation logic . In Proc. VMCAI-9 . Springer , 2008 . H. H. Nguyen, V. Kuncak, and W.-N. Chin. Runtime checking for separation logic. In Proc. VMCAI-9. Springer, 2008."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837621","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837621","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:37Z","timestamp":1750211017000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837621"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":29,"alternative-id":["10.1145\/2837614.2837621","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837621","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837621","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}