{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:56:12Z","timestamp":1725936972668},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_10","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"205-225","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["From Shapes to Amortized Complexity"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Fiedor","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moritz","family":"Sinn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Proc. of POPL 2009, pp. 239\u2013251 (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-37036-6_32","volume-title":"Programming Languages and Systems","author":"M Hofmann","year":"2013","unstructured":"Hofmann, M., Rodriguez, D.: Automatic type inference for amortised heap-space analysis. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 593\u2013613. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_32"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Logical Methods in Computer Science 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-28717-6_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., G\u00f3mez-Zamalloa, M., Puebla, G.: Automatic inference of resource consumption bounds. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 1\u201311. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28717-6_1"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-66845-1_6","volume-title":"Integrated Formal Methods","author":"F Frohn","year":"2017","unstructured":"Frohn, F., Giesl, J.: Complexity analysis for Java with AProVE. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 85\u2013101. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66845-1_6"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-662-46681-0_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Hol\u00edk","year":"2015","unstructured":"Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Forester: shape analysis using tree automata (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 432\u2013435. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_37"},{"key":"10_CR8","unstructured":"Sinn, M., Zuleger, F.: Loopus - a tool for computing loop bounds for c programs. In: Proc. of WING@ETAPS\/IJCAR (2010)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-662-46681-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Str\u00f6der","year":"2015","unstructured":"Str\u00f6der, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: termination and memory safety of C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 417\u2013419. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_32"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with Lists are Counter Automata. Formal Methods in System Design 38(2) (2011)","DOI":"10.1007\/s10703-011-0111-7"},{"key":"10_CR11","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). \nhttps:\/\/doi.org\/10.1007\/11817963_35"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Qadeer, S.: Verifying properties of well-founded linked lists. In: Proc. of POPL 2006. ACM Press (2006)","DOI":"10.1145\/1111037.1111048"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-45789-5_8","volume-title":"Static Analysis","author":"T Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 69\u201384. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45789-5_8"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. In: Proc. of POPL 2007. ACM (2007)","DOI":"10.1145\/1190216.1190249"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-540-27864-1_18","volume-title":"Static Analysis","author":"R Rugina","year":"2004","unstructured":"Rugina, R.: Quantitative shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 228\u2013245. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27864-1_18"},{"key":"10_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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-75596-8_12"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: Proc. of POPL 2010 (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-70545-1_41","volume-title":"Computer Aided Verification","author":"S Magill","year":"2008","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: THOR: a tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 428\u2013432. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-70545-1_41"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1007\/978-3-319-08867-9_50","volume-title":"Computer Aided Verification","author":"M Sinn","year":"2014","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745\u2013761. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_50"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-27813-9_29","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2004","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372\u2013386. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_29"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-36742-7_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 324\u2013338. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-36742-7_23"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-52234-0_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Hol\u00edk","year":"2017","unstructured":"Hol\u00edk, L., Hru\u0161ka, M., Leng\u00e1l, O., Rogalewicz, A., Vojnar, T.: Counterexample validation and interpolation-based refinement for forest automata. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 288\u2013309. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-52234-0_16"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/978-3-642-39799-8_52","volume-title":"Computer Aided Verification","author":"L Hol\u00edk","year":"2013","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 740\u2013755. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_52"},{"key":"10_CR24","unstructured":"Bj\u00f8rner, N.: The Z3 Theorem Prover. \nhttps:\/\/github.com\/Z3Prover\/z3\/"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:20:06Z","timestamp":1514434806000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}