{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:59:25Z","timestamp":1770274765956,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_12","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"131-146","source":"Crossref","is-referenced-by-count":39,"title":["Automated Cyclic Entailment Proofs in Separation Logic"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Dino","family":"Distefano","sequence":"additional","affiliation":[]},{"given":"Rasmus Lerchedahl","family":"Petersen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North-Holland, Amsterdam (1977)"},{"key":"12_CR2","unstructured":"Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh (November 2006)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-74061-2_6","volume-title":"Static Analysis","author":"J. Brotherston","year":"2007","unstructured":"Brotherston, J.: Formalised inductive reasoning in the logic of bunched implications. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 87\u2013103. Springer, Heidelberg (2007)"},{"key":"12_CR4","first-page":"101","volume-title":"Proceedings of POPL-35","author":"J. Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: Proceedings of POPL-35, pp. 101\u2013112. ACM, New York (2008)"},{"key":"12_CR5","first-page":"137","volume-title":"Proceedings of LICS-25","author":"J. Brotherston","year":"2010","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: Proceedings of LICS-25, pp. 137\u2013146. IEEE, New York (2010)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. Journal of Logic and Computation (2010)","DOI":"10.1093\/logcom\/exq052"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1016\/B978-044450813-3\/50015-1","volume-title":"Handbook of Automated Reasoning","author":"A. Bundy","year":"2001","unstructured":"Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol.\u00a0I, ch. 13, pp. 845\u2013911. Elsevier Science, Amsterdam (2001)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of POPL-36, pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"12_CR9","first-page":"366","volume-title":"Proceedings of LICS-22","author":"C. Calcagno","year":"2007","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: Proceedings of LICS-22, pp. 366\u2013378. IEEE, Los Alamitos (2007)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Evan Chang, B.-Y., Rival, X.: Relational inductive shape analysis. In: POPL 2008, pp. 247\u2013260 (2008)","DOI":"10.1145\/1328897.1328469"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B.-Y.E. Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 384\u2013401. Springer, Heidelberg (2007)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"12_CR13","first-page":"213","volume-title":"Proceedings of OOPSLA","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: Proceedings of OOPSLA, pp. 213\u2013226. ACM, New York (2008)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30142-4_7","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Dixon","year":"2004","unstructured":"Dixon, L., Fleuriot, J.D.: Higher order rippling in isaPlanner. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 83\u201398. Springer, Heidelberg (2004)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 60\u201366. Springer, Heidelberg (2009)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Haupstatz for the intuitionistic theory of iterated inductive definitions. In: Proc. Second Scandinavian Logic Symposium, pp. 179\u2013216 (1971)","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"12_CR17","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":"H.H. 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.\u00a05123, pp. 355\u2013369. Springer, Heidelberg (2008)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of 17th LICS (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Tuerk","year":"2009","unstructured":"Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 469\u2013484. Springer, Heidelberg (2009)"},{"key":"12_CR21","unstructured":"Voicu, R., Li, M.: Descente infinie proofs in Coq. In: Proceedings of the 1st Coq Workshop, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"issue":"1","key":"12_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/jigpal\/12.1.1","volume":"12","author":"C.-P. Wirth","year":"2004","unstructured":"Wirth, C.-P.: Descente Infinie + Deduction. Logic Journal of the IGPL\u00a012(1), 1\u201396 (2004)","journal-title":"Logic Journal of the IGPL"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:40Z","timestamp":1560381580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}