{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:05Z","timestamp":1776333485192,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662545768","type":"print"},{"value":"9783662545775","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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-662-54577-5_6","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T10:48:06Z","timestamp":1490870886000},"page":"99-117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Proving Termination Through Conditional Termination"],"prefix":"10.1007","author":[{"given":"Cristina","family":"Borralleras","sequence":"first","affiliation":[]},{"given":"Marc","family":"Brockschmidt","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Larraz","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"6_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., Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2\u201318. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-68863-1_2"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-15769-1_8"},{"key":"6_CR3","first-page":"47","volume":"215","author":"R Bagnara","year":"2012","unstructured":"Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. IC 215, 47\u201367 (2012)","journal-title":"IC"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-662-49674-9_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Bakhirkin","year":"2016","unstructured":"Bakhirkin, A., Piterman, N.: Finding recurrent sets with backward analysis and trace partitioning. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 17\u201335. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_2"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL (2013)","DOI":"10.1145\/2429069.2429078"},{"key":"6_CR6","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)"},{"issue":"3","key":"6_CR7","first-page":"1","volume":"10","author":"M Bozga","year":"2014","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Deciding conditional termination. LCMS 10(3), 1\u201361 (2014)","journal-title":"LCMS"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"AR 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. 3576, pp. 491\u2013504. Springer, Heidelberg (2005). doi:10.1007\/11513988_48"},{"key":"6_CR9","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. 8044, pp. 413\u2013429. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_28"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_22"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Joosten, S.J., Thiemann, R., Yamada, A.: Certifying safety and termination proofs for integer transition systems. In: WST (2016)","DOI":"10.1007\/978-3-319-63046-5_28"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Compositional safety verification with Max-SMT. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"6_CR13","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":"2011","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. 7421, pp. 123\u2013141. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-31762-0_9"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-Y Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156\u2013171. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_11"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-70545-1_32"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-21668-3_16","volume-title":"Computer Aided Verification","author":"V D\u2019Silva","year":"2015","unstructured":"D\u2019Silva, V., Urban, C.: Conflict-driven conditional termination. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 271\u2013286. Springer, Cham (2015). doi:10.1007\/978-3-319-21668-3_16"},{"key":"6_CR18","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: RTA (2011)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi:10.1007\/978-3-642-27705-4_21"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-12736-1_15","volume-title":"Programming Languages and Systems","author":"A Flores-Montoya","year":"2014","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275\u2013295. Springer, Cham (2014). doi:10.1007\/978-3-319-12736-1_15"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-39799-8_27","volume-title":"Computer Aided Verification","author":"P Ganty","year":"2013","unstructured":"Ganty, P., Genaim, S.: Proving termination starting from the end. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 397\u2013412. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_27"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. JAR (2016, to appear)","DOI":"10.1007\/s10817-016-9388-y"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: PLDI (2015)","DOI":"10.1145\/2737924.2737976"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL (2008)","DOI":"10.1145\/1328438.1328459"},{"key":"6_CR25","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":"WR 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. 6337, pp. 304\u2013319. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-15769-1_19"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/978-3-319-08867-9_53","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2014","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Termination analysis by learning terminating programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 797\u2013813. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_53"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-662-48899-7_38","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Kop","year":"2015","unstructured":"Kop, C., Nishida, N.: Constrained term rewriting tool. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 549\u2013557. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48899-7_38"},{"key":"6_CR28","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. 6174, pp. 89\u2013103. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_9"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1007\/978-3-319-08867-9_52","volume-title":"Computer Aided Verification","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779\u2013796. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_52"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-09284-3_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"D Larraz","year":"2014","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Minimal-model-guided approaches to solving polynomial constraints and extensions. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 333\u2013350. Springer, Cham (2014). doi:10.1007\/978-3-319-09284-3_25"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: PLDI (2015)","DOI":"10.1145\/2737924.2737993"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-54862-8_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Leike","year":"2014","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54862-8_12"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-54013-4_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Mass\u00e9","year":"2014","unstructured":"Mass\u00e9, D.: Policy iteration-based conditional termination and ranking functions. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 453\u2013471. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54013-4_25"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24622-0_20"},{"key":"6_CR36","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. 4354, pp. 245\u2013259. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-69611-7_16"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703\u2013719. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22110-1_57"},{"key":"6_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1007\/978-3-319-08867-9_50","volume-title":"Computer Aided Verification","author":"M Sinn","year":"2014","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745\u2013761. Springer, Cham (2014). doi:10.1007\/978-3-319-08867-9_50"},{"issue":"3","key":"6_CR39","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1709093.1709095","volume":"32","author":"F Spoto","year":"2010","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyser for Java Bytecode based on path-length. TOPLAS 32(3), 8:1\u20138:70 (2010)","journal-title":"TOPLAS"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). doi:10.1007\/978-3-319-08587-6_28"},{"key":"6_CR41","unstructured":"Termination Competition. http:\/\/termination-portal.org\/wiki\/Termination_Competition"},{"key":"6_CR42","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. 6605, pp. 81\u201395. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19835-9_9"},{"key":"6_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-38856-9_5","volume-title":"Static Analysis","author":"C Urban","year":"2013","unstructured":"Urban, C.: The abstract domain of segmented ranking functions. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 43\u201362. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38856-9_5"},{"key":"6_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-662-49674-9_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Urban","year":"2016","unstructured":"Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 54\u201370. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_4"},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-10936-7_19","volume-title":"Static Analysis","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302\u2013318. Springer, Cham (2014). doi:10.1007\/978-3-319-10936-7_19"},{"key":"6_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79124-9_11","volume-title":"Tests and Proofs","author":"H Velroyen","year":"2008","unstructured":"Velroyen, H., R\u00fcmmer, P.: Non-termination checking for imperative programs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154\u2013170. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-79124-9_11"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54577-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,21]],"date-time":"2021-04-21T02:27:34Z","timestamp":1618972054000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54577-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545768","9783662545775"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54577-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","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":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}