{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:14Z","timestamp":1763467874999},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705437"},{"type":"electronic","value":"9783540705451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_35","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"370-384","source":"Crossref","is-referenced-by-count":56,"title":["A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis"],"prefix":"10.1007","author":[{"given":"Bhargav S.","family":"Gulavani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"APRON. Numerical abstract domain library (2007), http:\/\/apron.cri.ensmp.fr\/library"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11547662_4","volume-title":"Static Analysis","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Rodr\u00edguez-Carbonell, E., Zaffanella, E.: Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 19\u201334. Springer, Heidelberg (2005)"},{"key":"35_CR3","unstructured":"Bagnara, R., Zaccagnini, A.: Checking and bounding the solutions of some recurrence relations. Quaderno 344, Universit\u00e0 di Parma, Italy (2004)"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11609773_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J.D. Bingham","year":"2005","unstructured":"Bingham, J.D., Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 207\u2013221. Springer, Heidelberg (2005)"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1349","DOI":"10.1007\/11523468_109","volume-title":"Automata, Languages and Programming","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1349\u20131361. Springer, Heidelberg (2005)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-30579-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 147\u2013163. Springer, Heidelberg (2005)"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-540-78739-6_13","volume-title":"ESOP 2008","author":"A. Chawdhary","year":"2008","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking abstractions. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 148\u2013162. Springer, Heidelberg (2008)"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"35_CR12","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI, pp. 376\u2013386 (2006)","DOI":"10.1145\/1133981.1134026"},{"key":"35_CR15","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: RTSS, pp. 57\u201366 (2006)","DOI":"10.1109\/RTSS.2006.12"},{"issue":"2","key":"35_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Methods Syst. Des.\u00a011(2), 157\u2013185 (1997)","journal-title":"Form. Methods Syst. Des."},{"issue":"2\/3","key":"35_CR17","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/A:1008189014032","volume":"18","author":"C.A. Healy","year":"2000","unstructured":"Healy, C.A., Sjodin, M., Rustagi, V., Whalley, D.B., van Engelen, R.: Supporting timing analysis by automatic bounding of loop iterations. Real-Time Systems\u00a018(2\/3), 129\u2013156 (2000)","journal-title":"Real-Time Systems"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"35_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"P.C. Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 104\u2013113. Springer, Heidelberg (1996)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/11817963_16","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2006","unstructured":"Kroening, D., Weissenbacher, G.: Counterexamples with loops for predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 152\u2013165. Springer, Heidelberg (2006)"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330\u2013341 (2004)","DOI":"10.1145\/964001.964029"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"35_CR23","first-page":"32","volume-title":"LICS","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE, Los Alamitos (2004)"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL, pp. 318\u2013329 (2004)","DOI":"10.1145\/964001.964028"},{"key":"35_CR25","doi-asserted-by":"crossref","unstructured":"Turing, A.: Checking a large routine, pp. 70\u201372 (1989)","DOI":"10.1093\/jaoac\/72.1.70"},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The Determination of Worst-Case Execution Times\u2014Overview of the Methods and Survey of Tools. ACM Transactions on Embedded Computing Systems (TECS) (2007)","DOI":"10.1145\/1347375.1347389"}],"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-540-70545-1_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T14:50:00Z","timestamp":1684507800000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}