{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T03:34:26Z","timestamp":1725680066321},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642297083"},{"type":"electronic","value":"9783642297090"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29709-0_20","type":"book-chapter","created":{"date-parts":[[2012,5,12]],"date-time":"2012-05-12T09:49:34Z","timestamp":1336816174000},"page":"227-242","source":"Crossref","is-referenced-by-count":21,"title":["Symbolic Loop Bound Computation for WCET Analysis"],"prefix":"10.1007","author":[{"given":"Jens","family":"Knoop","sequence":"first","affiliation":[]},{"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[]},{"given":"Jakob","family":"Zwirchmayr","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E. Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. J. Automated Reasoning\u00a046(2), 161\u2013203 (2011)","journal-title":"J. Automated Reasoning"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Ammarguellat, Z., Harrison III., W.L.: Automatic Recognition of Induction Variables and Recurrence Relations by Abstract Interpretation. In: Proc. of PLDI, pp. 283\u2013295 (1990)","DOI":"10.1145\/93548.93583"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-17511-4_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Blanc","year":"2010","unstructured":"Blanc, R., Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L.: ABC: Algebraic Bound Computation for Loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 103\u2013118. Springer, Heidelberg (2010)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, vol.\u00a0104. American Mathematical Society (2003)","DOI":"10.1090\/surv\/104"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: Proc. of POPL, pp. 127\u2013139 (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The Reachability-Bound Problem. In: Proc. of PLDI, pp. 292\u2013304 (2010)","DOI":"10.1145\/1809028.1806630"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Gustafsson, J., Ermedahl, A., Sandberg, C., Lisper, B.: Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. In: Proc. of RTSS, pp. 57\u201366 (2006)","DOI":"10.1109\/RTSS.2006.12"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Hottelier, T., Kov\u00e1cs, L.: Valigator: A Verification Tool with Bound and Invariant Generation. In: Proc. of LPAR-15, pp. 333\u2013342 (2008)","DOI":"10.1007\/978-3-540-89439-1_24"},{"key":"20_CR10","unstructured":"Holsti, N., Gustafsson, J., Bernat, G., Ballabriga, C., Bonenfant, A., Bourgade, R., Cass\u00e9, H., Cordes, D., Kadlec, A., Kirner, R., Knoop, J., Lokuciejewski, P., Merriam, N., de Michiel, M., Prantl, A., Rieder, B., Rochange, C., Sainrat, P., Schordan, M.: WCET 2008 - Report from the Tool Challenge 2008 - 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. In: Proc. of WCET (2008)"},{"issue":"9","key":"20_CR11","doi-asserted-by":"publisher","first-page":"1039","DOI":"10.1016\/j.jsc.2006.06.005","volume":"41","author":"M. Kauers","year":"2006","unstructured":"Kauers, M.: SumCracker: A Package for Manipulating Symbolic Sums and Related Objects. J. of Symbolic Computation\u00a041(9), 1039\u20131057 (2006)","journal-title":"J. of Symbolic Computation"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Kirner, R., Knoop, J., Prantl, A., Schordan, M., Kadlec, A.: Beyond Loop Bounds: Comparing Annotation Languages for Worst-Case Execution Time Analysis. J. of Software and System Modeling (2010); Online edition","DOI":"10.1007\/s10270-010-0161-0"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"20_CR14","unstructured":"Lisper, B.: Fully Automatic, Parametric Worst-Case Execution Time Analysis. In: Proc. of WCET, pp. 99\u2013102 (2003)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Michiel, M.D., Bonenfant, A., Cass\u00e9, H., Sainrat, P.: Static Loop Bound Analysis of C Programs Based on Flow Analysis and Abstract Interpretation. In: Proc. of RTCSA, pp. 161\u2013166 (2008)","DOI":"10.1109\/RTCSA.2008.53"},{"issue":"5-6","key":"20_CR16","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1006\/jsco.1995.1071","volume":"20","author":"P. Paule","year":"1995","unstructured":"Paule, P., Schorn, M.: A Mathematica Version of Zeilberger\u2019s Algorithm for Proving Binomial Coefficient Identities. J. of Symbolic Computation\u00a020(5-6), 673\u2013698 (1995)","journal-title":"J. of Symbolic Computation"},{"key":"20_CR17","unstructured":"Prantl, A.: High-level Compiler Support for Timing-Analysis. PhD thesis, Vienna University of Technology (2010)"},{"key":"20_CR18","unstructured":"Prantl, A., Knoop, J., Kirner, R., Kadlec, A., Schordan, M.: From Trusted Annotations to Verified Knowledge. In: Proc. of WCET, pp. 39\u201349 (2009)"},{"key":"20_CR19","unstructured":"Prantl, A., Knoop, J., Schordan, M., Triska, M.: Constraint Solving for High-Level WCET Analysis. In: Proc. of WLPE, pp. 77\u201389 (2008)"},{"key":"20_CR20","unstructured":"Prantl, A., Schordan, M., Knoop, J.: TuBound - A Conceptually New Tool for WCET Analysis. In: Proc. of WCET, pp. 141\u2013148 (2008)"},{"issue":"2-3","key":"20_CR21","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Schneider, C.: Symbolic Summation with Single-Nested Sum Extensions. In: Proc. of ISSAC, pp. 282\u2013289 (2004)","DOI":"10.1145\/1005285.1005326"},{"key":"20_CR23","unstructured":"Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media (2003)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of Systems Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29709-0_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:21Z","timestamp":1620126861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29709-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642297083","9783642297090"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29709-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}