{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:08:42Z","timestamp":1725746922206},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_24","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T05:11:21Z","timestamp":1377753081000},"page":"334-348","source":"Crossref","is-referenced-by-count":2,"title":["Control Flow Refinement and Symbolic Computation of Average Case Bound"],"prefix":"10.1007","author":[{"given":"Hong Yi","family":"Chen","sequence":"first","affiliation":[]},{"given":"Supratik","family":"Mukhopadhyay","sequence":"additional","affiliation":[]},{"given":"Zheng","family":"Lu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","first-page":"49","volume-title":"Proceedings of the Seventh ACM International Conference on Embedded Software, EMSOFT 2009","author":"G. Balakrishnan","year":"2009","unstructured":"Balakrishnan, G., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Refining the control structure of loops using static analysis. In: Proceedings of the Seventh ACM International Conference on Embedded Software, EMSOFT 2009, pp. 49\u201358. ACM, New York (2009)"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","key":"24_CR2","DOI":"10.1145\/512950.512973"},{"key":"24_CR3","first-page":"395","volume-title":"Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE 2007","author":"S.F. Goldsmith","year":"2007","unstructured":"Goldsmith, S.F., Aiken, A.S., Wilkerson, D.S.: Measuring empirical computational complexity. In: Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE 2007, pp. 395\u2013404. ACM, New York (2007)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-70545-1_35","volume-title":"Computer Aided Verification","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 370\u2013384. Springer, Heidelberg (2008)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02658-4_7","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 51\u201362. Springer, Heidelberg (2009)"},{"key":"24_CR6","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1145\/1543135.1542518","volume":"44","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. SIGPLAN Not.\u00a044, 375\u2013385 (2009)","journal-title":"SIGPLAN Not."},{"key":"24_CR7","first-page":"127","volume-title":"Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 127\u2013139. ACM, New York (2009)"},{"issue":"6","key":"24_CR8","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/1809028.1806630","volume":"45","author":"Sumit Gulwani","year":"2010","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292\u2013304 (2010)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR9","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/A:1008189014032","volume":"18","author":"C. Healy","year":"2000","unstructured":"Healy, C., Sj\u00f6din, M., Rustagi, V., Whalley, D., Van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Syst.\u00a018, 129\u2013156 (2000)","journal-title":"Real-Time Syst."},{"unstructured":"Knuth, D.E.: The Art of Computer Programming, 2nd edn. Fundamental Algorithms, vol.\u00a0I. Addison-Wesley (1973)","key":"24_CR10"},{"unstructured":"Kr\u00f6ning, D.: Cprover benchmarking toolkit, \n                    \n                      http:\/\/www.cprover.org\/software\/benchmarks\/","key":"24_CR11"},{"issue":"2","key":"24_CR12","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1145\/42190.42347","volume":"10","author":"D. M\u00e9tayer Le","year":"1988","unstructured":"Le M\u00e9tayer, D.: Ace: An automatic complexity evaluator. ACM Trans. Program. Lang. Syst.\u00a010(2), 248\u2013266 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Rosendahl, M.: Automatic complexity analysis. In: FPCA, pp. 144\u2013156 (1989)","key":"24_CR14","DOI":"10.1145\/99370.99381"},{"issue":"9","key":"24_CR15","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B. Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM\u00a018(9), 528\u2013539 (1975)","journal-title":"Commun. ACM"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1145\/321978.321987","volume":"23","author":"B. Wegbreit","year":"1976","unstructured":"Wegbreit, B.: Verifying program performance. J. ACM\u00a023, 691\u2013699 (1976)","journal-title":"J. ACM"},{"issue":"3","key":"24_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"Reinhard Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution time problem\u2014overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (TECS)\u00a07(3) (2008)","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-70545-1_6","volume-title":"Computer Aided Verification","author":"R. Wilhelm","year":"2008","unstructured":"Wilhelm, R., Wachter, B.: Abstract interpretation with applications to timing validation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 22\u201336. Springer, Heidelberg (2008)"},{"key":"24_CR19","volume-title":"The Mathematica Book","author":"S. Wolfram","year":"2003","unstructured":"Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media, Incorporated (2003)","edition":"5"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-69166-2_15","volume-title":"Static Analysis","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 221\u2013237. Springer, Heidelberg (2008)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-33125-1_28","volume-title":"Static Analysis","author":"H.Y. Chen","year":"2012","unstructured":"Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 422\u2013438. Springer, Heidelberg (2012)"},{"unstructured":"Cook, B., Gulwani, S., Lev-ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination (2008)","key":"24_CR23"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-88387-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 111\u2013125. Springer, Heidelberg (2008)"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"24_CR26","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1145\/322261.322273","volume":"28","author":"R.E. Tarjan","year":"1981","unstructured":"Tarjan, R.E.: Fast algorithms for solving path problems. J. ACM\u00a028, 594\u2013614 (1981)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:25:13Z","timestamp":1558052713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}