{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:33:28Z","timestamp":1752986008798,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319694825"},{"type":"electronic","value":"9783319694832"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-69483-2_9","type":"book-chapter","created":{"date-parts":[[2017,10,16]],"date-time":"2017-10-16T11:34:48Z","timestamp":1508153688000},"page":"147-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Computing Exact Loop Bounds for Bounded Program Verification"],"prefix":"10.1007","author":[{"given":"Tianhai","family":"Liu","sequence":"first","affiliation":[]},{"given":"Shmuel","family":"Tyszberowicz","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[]},{"given":"Mana","family":"Taghdiri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,17]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification \u2013 The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-49812-6","key":"9_CR1","DOI":"10.1007\/978-3-319-49812-6"},{"unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, The University of Iowa (2015)","key":"9_CR2"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: vZ - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_14"},{"key":"9_CR4","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 2010. LNCS, vol. 6355, pp. 103\u2013118. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_7"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_7"},{"unstructured":"Cullmann, C., Martin, F.: Data-flow based detection of loop bounds. In: WCET. OASICS, vol. 6. Schloss Dagstuhl (2007)","key":"9_CR6"},{"unstructured":"Dennis, G.D.: A Relational Framework for Bounded Program Verification. Ph.D. thesis, MIT (2009)","key":"9_CR7"},{"key":"9_CR8","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":"BS 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. 5123, pp. 370\u2013384. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_35"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI, pp. 375\u2013385. ACM (2009)","key":"9_CR9","DOI":"10.1145\/1543135.1542518"},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127\u2013139. ACM (2009)","key":"9_CR10","DOI":"10.1145\/1594834.1480898"},{"doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Weissenbacher, G.: Incremental bounded software model checking. In: SPIN, pp. 40\u201347. ACM (2014)","key":"9_CR11","DOI":"10.1145\/2632362.2632374"},{"key":"9_CR12","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"D Jackson","year":"2016","unstructured":"Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT, Cambridge (2016)"},{"issue":"3","key":"9_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"doi-asserted-by":"crossref","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: POPL, pp. 607\u2013618. ACM (2014)","key":"9_CR14","DOI":"10.1145\/2535838.2535857"},{"doi-asserted-by":"crossref","unstructured":"Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: ICST, pp. 101\u2013110. IEEE (2012)","key":"9_CR15","DOI":"10.1109\/ICST.2012.90"},{"doi-asserted-by":"crossref","unstructured":"Lokuciejewski, P., Cordes, D., Falk, H., Marwedel, P.: A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models. In: CGO, pp. 136\u2013146. IEEE (2009)","key":"9_CR16","DOI":"10.1109\/CGO.2009.17"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-29700-7_23","volume-title":"Frontiers in Algorithmics and Algorithmic Aspects in Information and Management","author":"F Ma","year":"2012","unstructured":"Ma, F., Yan, J., Zhang, J.: Solving generalized optimization problems subject to SMT constraints. In: Snoeyink, J., Lu, P., Su, K., Wang, L. (eds.) AAIM\/FAW -2012. LNCS, vol. 7285, pp. 247\u2013258. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-29700-7_23"},{"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: RTCSA, pp. 161\u2013166. IEEE (2008)","key":"9_CR18","DOI":"10.1109\/RTCSA.2008.53"},{"key":"9_CR19","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","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with LA (Q) cost functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 484\u2013498. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_38"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-21690-4_27","volume-title":"Computer Aided Verification","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 447\u2013454. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_27"},{"doi-asserted-by":"crossref","unstructured":"Shkaravska, O., Kersten, R., van Eekelen, M.: Test-based inference of polynomial loop-bound functions. In: PPPJ, pp. 99\u2013108. ACM (2010)","key":"9_CR22","DOI":"10.1145\/1852761.1852776"},{"unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L.J., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: CASCON, p. 13. IBM (1999)","key":"9_CR23"},{"unstructured":"Vaziri, M.: Finding Bugs in Software with a Constraint Solver. Ph.D. thesis, MIT (2004)","key":"9_CR24"},{"unstructured":"Termination problems data base (TPDB). http:\/\/termination-portal.org\/wiki\/TPDB . Accessed June 2017","key":"9_CR25"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-69483-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T14:18:13Z","timestamp":1750947493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-69483-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319694825","9783319694832"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-69483-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"17 October 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Changsha","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lcs.ios.ac.cn\/setta2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}