{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:36Z","timestamp":1777890996141,"version":"3.51.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319522333","type":"print"},{"value":"9783319522340","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_25","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"462-482","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning in the Bernays-Sch\u00f6nfinkel-Ramsey Fragment of Separation Logic"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Serban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-662-46669-8_26","volume-title":"Programming Languages and Systems","author":"A Albargouthi","year":"2015","unstructured":"Albargouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 634\u2013660. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-662-46669-8_26"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21\u201352 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1016\/j.ic.2011.12.003","volume":"211","author":"R Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"issue":"6","key":"25_CR5","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 21(6), 1177\u20131216 (2011)","journal-title":"J. Logic Comput."},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-20398-5_33","volume-title":"NASA Formal Methods","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D.: Infer: an automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 459\u2013465. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-20398-5_33"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108\u2013119. Springer, Heidelberg (2001). doi:\n                    10.1007\/3-540-45294-X_10"},{"key":"25_CR8","unstructured":"Demri, S., Deters, M.: Two-variable separation logic and its inner circle. ACM Trans. Comput. Logic 16(2) (2015). Article no. 15"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-06686-8_10","volume-title":"Computer Science - Theory and Applications","author":"S Demri","year":"2014","unstructured":"Demri, S., Galmiche, D., Larchey-Wendling, D., M\u00e9ry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.\u00c9., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125\u2013138. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-319-06686-8_10"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-22110-1_29","volume-title":"Computer Aided Verification","author":"K Dudka","year":"2011","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 372\u2013378. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-22110-1_29"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1093\/logcom\/exn066","volume":"20","author":"D Galmiche","year":"2010","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189\u2013231 (2010)","journal-title":"J. Logic Comput."},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Berlin (2004). doi:\n                    10.1007\/978-3-540-27813-9_14"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-02658-4_25"},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is \n                    \n                      \n                    \n                    $$\\pi ^1_1$$\n                   complete. J. Symbolic Logic 56(2), 637\u2013642 (1991)","journal-title":"J. Symbolic Logic"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/373243.375719","volume":"36","author":"SS Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures. ACM SIGPLAN Not. 36, 14\u201326 (2001)","journal-title":"ACM SIGPLAN Not."},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: Proceedings of 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Sydney, Australia, 12\u201315 August 2008, pp. 292\u2013298 (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"issue":"3","key":"25_CR17","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"HR Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"25_CR18","first-page":"354","volume":"11","author":"Y Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.: Enumerable sets are diophantine. J. Sovietic Math. 11, 354\u2013358 (1970)","journal-title":"J. Sovietic Math."},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-70545-1_34","volume-title":"Computer Aided Verification","author":"HH Nguyen","year":"2008","unstructured":"Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355\u2013369. Springer, Heidelberg (2008). doi:\n                    10.1007\/978-3-540-70545-1_34"},{"issue":"4","key":"25_CR20","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 773\u2013789. Springer, Heidelberg (2013). doi:\n                    10.1007\/978-3-642-39799-8_54"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating Separation Logic with Trees and Data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 711\u2013728. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-319-08867-9_47"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counter example-guided quantifier instantiation for synthesis in SMT. In: Proceedings of Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, 18\u201324 July 2015, Part II, pp. 198\u2013216 (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"25_CR24","unstructured":"Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays-Schoenfinkel-Ramsey fragment of separation logic. CoRR abs\/1610.04707 (2016). \n                    http:\/\/arxiv.org\/abs\/1610.04707"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, Chiba, Japan, 17\u201320 October 2016, pp. 244\u2013261 (2016)","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). doi:\n                    10.1007\/978-3-642-39799-8_42"},{"key":"25_CR27","unstructured":"Sighireanu, M., Cok, D.: Report on SL-COMP 2014. J. Satisfiability Boolean Model. Comput. 1 (2014)"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-10936-7_18","volume-title":"Static Analysis","author":"A Toubhans","year":"2014","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: An abstract domain combinator for separately conjoining memory abstractions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 285\u2013301. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-319-10936-7_18"},{"key":"25_CR29","unstructured":"Voigt, M., Weidenbach, C.: Bernays-Sch\u00f6nfinkel-Ramsey with simple bounds is nexptime-complete. CoRR abs\/1501.07209 (2015)"},{"key":"25_CR30","unstructured":"Yang, H.: Local reasoning for stateful programs. Ph.D. thesis, University of Illinois at Urbana-Champaign (2001)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:10:14Z","timestamp":1558318214000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.researchr.org\/home\/VMCAI-2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}