{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:05:28Z","timestamp":1746331528056,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319085869"},{"type":"electronic","value":"9783319085876"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08587-6_15","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T03:38:32Z","timestamp":1404272312000},"page":"208-223","source":"Crossref","is-referenced-by-count":8,"title":["Proving Termination and Memory Safety for Programs with Pointer Arithmetic"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Str\u00f6der","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Frohn","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Fuhs","sequence":"additional","affiliation":[]},{"given":"Jera","family":"Hensel","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-68863-1_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 2\u201318. Springer, Heidelberg (2008)"},{"key":"15_CR2","unstructured":"AProVE, http:\/\/aprove.informatik.rwth-aachen.de\/eval\/Pointer\/"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-22110-1_15","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2011","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 178\u2013183. Springer, Heidelberg (2011)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31762-0_9","volume-title":"Formal Verification of Object-Oriented Software","author":"M. Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Str\u00f6der, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for JBC. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 123\u2013141. Springer, Heidelberg (2012)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-31424-7_13","volume-title":"Computer Aided Verification","author":"M. Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 105\u2013122. Springer, Heidelberg (2012)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-35182-2_25","volume-title":"Programming Languages and Systems","author":"J. Brotherston","year":"2012","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol.\u00a07705, pp. 350\u2013367. Springer, Heidelberg (2012)"},{"key":"15_CR8","unstructured":"Clang compiler, http:\/\/clang.llvm.org"},{"key":"15_CR9","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: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) POPL 1977, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-54862-8_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Dudka","year":"2014","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 412\u2013414. Springer, Heidelberg (2014)"},{"key":"15_CR11","unstructured":"Dutertre, B., de Moura, L.M.: The Yices SMT solver (2006), http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"15_CR12","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. Dagstuhl Publishing (2011)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/978-3-642-36742-7_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Falke","year":"2013","unstructured":"Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 623\u2013626. Springer, Heidelberg (2013)"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-15769-1_19","volume-title":"Static Analysis","author":"W.R. Harris","year":"2010","unstructured":"Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 304\u2013319. Springer, Heidelberg (2010)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a08172, pp. 365\u2013380. Springer, Heidelberg (2013)"},{"key":"15_CR16","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":"15_CR17","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":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-54862-8_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. L\u00f6we","year":"2014","unstructured":"L\u00f6we, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 392\u2013394. Springer, Heidelberg (2014)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.H., Lee, P., Tsay, Y.K.: Automatic numeric abstractions for heap-manipulating programs. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL 2010, pp. 211\u2013222. ACM Press (2010)","DOI":"10.1145\/1707801.1706326"},{"key":"15_CR20","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"11","key":"15_CR21","doi-asserted-by":"publisher","first-page":"1184","DOI":"10.1016\/j.jsc.2010.06.004","volume":"45","author":"Y. Moy","year":"2010","unstructured":"Moy, Y., March\u00e9, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput.\u00a045(11), 1184\u20131211 (2010)","journal-title":"J. Symb. Comput."},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"15_CR23","unstructured":"http:\/\/fxr.watson.org\/fxr\/source\/lib\/libsa\/strlen.c?v=OPENBSD"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS\u00a032(3) (2010)","DOI":"10.1145\/1709093.1709095"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Str\u00f6der, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Automated termination analysis for programs with pointer arithmetic. Tech. Rep. AIB 2014-05 available from [2] and from http:\/\/aib.informatik.rwth-aachen.de","DOI":"10.1007\/978-3-319-08587-6_15"},{"key":"15_CR27","unstructured":"SV-COMP at TACAS 2014, http:\/\/sv-comp.sosy-lab.org\/2014\/"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-19835-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tsitovich","year":"2011","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 81\u201395. Springer, Heidelberg (2011)"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 43\u201362. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"15_CR30","unstructured":"Wikibooks C Programming, http:\/\/en.wikibooks.org\/wiki\/C_Programming\/"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM IR for verified program transformations. In: Field, J., Hicks, M. (eds.) POPL 2012, pp. 427\u2013440. ACM Press (2012)","DOI":"10.1145\/2103621.2103709"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08587-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:40:48Z","timestamp":1746290448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08587-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319085869","9783319085876"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08587-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}