{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T03:44:59Z","timestamp":1743133499702,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415277"},{"type":"electronic","value":"9783319415284"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_23","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"426-446","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["From Shape Analysis to Termination Analysis in Linear Time"],"prefix":"10.1007","author":[{"given":"Roman","family":"Manevich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Dogadov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"23_CR1","volume-title":"Compilers: Principles,Techniques and Tools","author":"AV Aho","year":"1988","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles,Techniques and Tools. Addison-Wesley, Reading (1988)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-68863-1_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"E Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2\u201318. Springer, Heidelberg (2008)"},{"key":"23_CR3","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. 3780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 211\u2013224 (2007)","DOI":"10.1145\/1190215.1190249"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"23_CR6","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/978-3-642-31424-7_13","volume-title":"Computer Aided Verification","author":"Marc Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: International Conference on Computer Aided Verification, pp. 105\u2013122 (2012)"},{"key":"23_CR7","unstructured":"Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java bytecode programs by term rewriting. In: International Conference on Rewriting Techniques and Applications, pp. 155\u2013170 (2011)"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 101\u2013112 (2008)","DOI":"10.1145\/1328897.1328453"},{"key":"23_CR9","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.) Static Analysis. LNCS, vol. 8723, pp. 68\u201384. Springer, Heidelberg (2014)"},{"issue":"6","key":"23_CR10","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)","journal-title":"J. ACM"},{"key":"23_CR11","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"23_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.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Gies","year":"2014","unstructured":"Gies, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184\u2013191. Springer, Heidelberg (2014)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 239\u2013251 (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Guo, B., Vachharajani, N., August, D.I.: Shape analysis with inductive recursion synthesis. In: ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 256\u2013265 (2007)","DOI":"10.1145\/1273442.1250764"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-75596-8_12","volume-title":"Automated Technology for Verification and Analysis","author":"P Habermehl","year":"2007","unstructured":"Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving termination of tree manipulating programs. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 145\u2013161. Springer, Heidelberg (2007)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: a framework for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280\u2013301. Springer, Berlin (2000)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/11823230_17","volume-title":"Static Analysis","author":"A Loginov","year":"2006","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261\u2013279. Springer, Heidelberg (2006)"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 211\u2013222 (2010)","DOI":"10.1145\/1707801.1706326"},{"key":"23_CR20","volume-title":"Advanced Compiler Design and Implementation","author":"SS Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers Inc., San Francisco (1997)"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java bytecode by term rewriting. In: International Conference on Rewriting Techniques and Applications, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-70545-1_31","volume-title":"Computer Aided Verification","author":"A Podelski","year":"2008","unstructured":"Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 314\u2013327. Springer, Heidelberg (2008)"},{"issue":"3","key":"23_CR23","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/1353445.1353447","volume":"30","author":"N Rinetzky","year":"2008","unstructured":"Rinetzky, N., Ramalingam, G., Sagiv, M., Yahav, E.: On the complexity of partially-flow-sensitive alias analysis. ACM Trans. Program. Lang. Syst. 30(3), 13:1\u201313:28 (2008)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 133\u2013149. Springer, Heidelberg (2001)"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Rival, X., Chang, B.-Y.E.: Calling context abstraction with shapes. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 173\u2013186 (2011)","DOI":"10.1145\/1925844.1926406"},{"issue":"3","key":"23_CR26","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"23_CR27","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1709093.1709095","volume":"32","author":"F Spoto","year":"2010","unstructured":"Spoto, F., Mesnard, F., Payet, E.: A termination analyzer for Java bytecode based on path-length. ACM Trans. Program. Lang. Syst. 32(3), 8:1\u20138:70 (2010)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-35873-9_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Toubhans","year":"2013","unstructured":"Toubhans, A., Chang, B.-Y.E., Rival, X.: Reduced product combination of abstract domains for shapes. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 375\u2013395. Springer, Heidelberg (2013)"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) Static Analysis. LNCS, vol. 8723, pp. 285\u2013301. Springer, Heidelberg (2014)"},{"key":"23_CR30","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"Eran Yahav","year":"2003","unstructured":"Yahav, E., Reps, T.W., Sagiv, S., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: European Symposium on Programming, pp. 204\u2013222 (2003)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41528-4_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:05:50Z","timestamp":1594685150000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}