{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:43Z","timestamp":1748664523384,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_20","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"287-303","source":"Crossref","is-referenced-by-count":2,"title":["Disproving Inductive Entailments in Separation Logic via Base Pair Approximation"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[]},{"given":"Nikos","family":"Gorogiannis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"20_CR1","unstructured":"Cyclist: software distribution for this paper, https:\/\/github.com\/ngorogiannis\/cyclist\/releases\/tag\/TABLEAUX15"},{"key":"20_CR2","unstructured":"The first Separation Logic Competition (SL-COMP14), http:\/\/www.liafa.univ-paris-diderot.fr\/~sighirea\/slcomp14\/"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-642-54830-7_27","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Antonopoulos","year":"2014","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol.\u00a08412, pp. 411\u2013425. Springer, Heidelberg (2014)"},{"issue":"7","key":"20_CR4","doi-asserted-by":"publisher","first-page":"411","DOI":"10.2307\/2300300","volume":"41","author":"E. Bell","year":"1934","unstructured":"Bell, E.: Exponential numbers. The American Mathematical Monthly\u00a041(7), 411\u2013419 (1934)","journal-title":"The American Mathematical Monthly"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proc. POPL-32, pp. 59\u201370. ACM (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"20_CR9","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":"20_CR10","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Fuhs, C., Gorogiannis, N., Navarro P\u00e9rez, J.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proc. CSL-LICS, pp. 25:1\u201325:10. ACM (2014)","DOI":"10.1145\/2603088.2603091"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-319-10936-7_5","volume-title":"Static Analysis","author":"J. Brotherston","year":"2014","unstructured":"Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 68\u201384. Springer, Heidelberg (2014)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Gorogiannis, N., Kanovich, M., Rowe, R.: Model checking for symbolic-heap separation logic with inductive predicates (2015) (submitted)","DOI":"10.1145\/2837614.2837621"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-35182-2_25","volume-title":"Programming Languages and Systems","author":"J. Brotherston","year":"2012","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol.\u00a07705, pp. 350\u2013367. Springer, Heidelberg (2012)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. Journal of the ACM\u00a058(6) (2011)","DOI":"10.1145\/2049697.2049700"},{"issue":"9","key":"20_CR15","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W.-N. Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming\u00a077(9), 1006\u20131036 (2012)","journal-title":"Science of Computer Programming"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K. Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 392\u2013406. Springer, Heidelberg (2013)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Hurlin, C., Bobot, F., Summers, A.J.: Size does matter: Two certified abstractions to disprove entailment in intuitionistic and classical separation logic. In: Proc. IWACO, pp. 5:1\u20135:6. ACM (2009)","DOI":"10.1145\/1562154.1562159"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In: Proc. POPL-37, pp. 211\u2013222. ACM (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Pek, E., Qiu, X., Madhusudan, P.: Natural proofs for data structure manipulation in C using separation logic. In: Proc. PLDI-35, pp. 440\u2013451. ACM (2014)","DOI":"10.1145\/2666356.2594325"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS-17, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T14:54:28Z","timestamp":1748616868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}