{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T04:23:28Z","timestamp":1782879808440,"version":"3.54.5"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415901","type":"print"},{"value":"9783319415918","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_16","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T17:27:27Z","timestamp":1466702847000},"page":"234-252","source":"Crossref","is-referenced-by-count":6,"title":["Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution"],"prefix":"10.1007","author":[{"given":"Jera","family":"Hensel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Str\u00f6der","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"16_CR1","unstructured":"AProVE. http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Bitvectors\/"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Chen, H.Y., David, C., Kroening, D., Schrammel, P., W\u00e4chter, B.: Synthesising interprocedural bit-precise termination proofs. In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) ASE 2015, pp. 53\u201364. IEEE (2015)","DOI":"10.1109\/ASE.2015.10"},{"key":"16_CR3","unstructured":"Clang compiler. http:\/\/clang.llvm.org"},{"issue":"1","key":"16_CR4","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s10703-013-0186-4","volume":"43","author":"B Cook","year":"2013","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.: Ranking function synthesis for bit-vector relations. Formal Methods Syst. Des. 43(1), 93\u2013120 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-662-46669-8_8","volume-title":"Programming Languages and Systems","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 183\u2013204. Springer, Heidelberg (2015)"},{"key":"16_CR6","unstructured":"Dutertre, B., de Moura, L.M.: The Yices SMT solver (2006). Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"16_CR7","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Schmidt-Schau\u00df, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 41\u201350 (2011)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-642-27705-4_21","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Falke","year":"2012","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 261\u2013277. Springer, Heidelberg (2012)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., et al.: Proving termination of programs automatically with $$\\sf AProVE$$ . In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 184\u2013191. Springer, Heidelberg (2014)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Heidelberg (2013)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75\u201388. IEEE (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-319-08587-6_15","volume-title":"Automated Reasoning","author":"T Str\u00f6der","year":"2014","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 208\u2013223. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:57:27Z","timestamp":1498323447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}