{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T16:07:06Z","timestamp":1768320426472,"version":"3.49.0"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216898","type":"print"},{"value":"9783319216904","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_4","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"49-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":41,"title":["Fairness Modulo Theory: A New Approach to LTL Software Model Checking"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Langenfeld","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"4_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P., et al.: Principles of Model Checking, vol. 26202649. MIT Press, Cambridge (2008)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"issue":"1","key":"4_CR3","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. STTT 5(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"4_CR4","series-title":"LNCS","first-page":"863","volume-title":"CAV 2013","author":"J Barnat","year":"2013","unstructured":"Barnat, J., Brim, L., Havel, V., Havl\u00ed\u010dek, J., Kriho, J., Len\u010do, M., Ro\u010dkai, P., \u0160till, V., Weiser, J.: DiVinE 3.0 \u2013 an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/978-3-319-14896-0_5","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"P Bauch","year":"2014","unstructured":"Bauch, P., Havel, V., Barnat, J.: LTL model checking of LLVM bitcode with symbolic data. In: Hlin\u011bn\u00fd, P., Dvo\u0159\u00e1k, Z., Jaro\u0161, J., Kofro\u0148, J., Ko\u0159enek, J., Matula, P., Pala, K. (eds.) MEMICS 2014. LNCS, vol. 8934, pp. 47\u201359. Springer, Heidelberg (2014)"},{"key":"4_CR6","unstructured":"Baudin, P., Filli\u00e2tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V., et al.: ACSL: ANSI\/ISO C specification language, Feb 2015. http:\/\/frama-c.com\/download.html"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-02658-4_12","volume-title":"Computer Aided Verification","author":"AM Ben-Amram","year":"2009","unstructured":"Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 109\u2013123. Springer, Heidelberg (2009)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL, pp. 51\u201362 (2013)","DOI":"10.1145\/2480359.2429078"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386\u2013400. Springer, Heidelberg (2006)","DOI":"10.1007\/11817963_35"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401\u2013416. Springer, Heidelberg (2015)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332, IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"4_CR12","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)"},{"issue":"4","key":"4_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s10817-011-9237-y","volume":"47","author":"A Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free presburger arithmetic. J. Autom. Reason. 47(4), 341\u2013367 (2011)","journal-title":"J. Autom. Reason."},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"4_CR15","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.-J.: Symbolic model checking: $$10^{20}$$ states and beyond. In: LICS, pp. 428\u2013439, IEEE (1990)"},{"key":"4_CR16","unstructured":"Christ, J., Dietsch, D., Ermis, E., Heizmann, M., Hoenicke, J., Langenfeld, V., Leike, J., Musa, B., Nutz, A., Schilling, C.: The program analysis framework ultimate, Feb 2015. http:\/\/ultimate.informatik.uni-freiburg.de"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"4_CR19","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 (ETAPS 2013). LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"4_CR20","series-title":"LNCS","first-page":"154","volume-title":"CAV 2000","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/1190215.1190257","volume":"42","author":"B Cook","year":"2007","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. ACM SIGPLAN Not. 42, 265\u2013276 (2007). ACM","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/978-3-662-46681-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 384\u2013398. Springer, Heidelberg (2015)"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1145\/1925844.1926431","volume":"46","author":"B Cook","year":"2011","unstructured":"Cook, B., Koskinen, E.: Making prophecies with decision predicates. ACM SIGPLAN Not. 46, 399\u2013410 (2011). ACM","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"4_CR24","first-page":"66","volume":"41","author":"B Cook","year":"2012","unstructured":"Cook, B., Koskinen, E., Vardi, M.Y.: Temporal property verification as a program analysis task - extended version. FMSD 41(1), 66\u201382 (2012)","journal-title":"FMSD"},{"issue":"1","key":"4_CR25","first-page":"93","volume":"43","author":"B Cook","year":"2013","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. FMSD 43(1), 93\u2013120 (2013)","journal-title":"FMSD"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426, ACM (2006)","DOI":"10.1145\/1133255.1134029"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: PLDI, pp. 320\u2013330 (2007)","DOI":"10.1145\/1273442.1250771"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Zheng, H., et al.: Bandera: extracting finite-state models from Java source code. In: ICSE, pp. 439\u2013448, IEEE (2000)","DOI":"10.1145\/337180.337234"},{"key":"4_CR29","series-title":"LNCS","first-page":"423","volume-title":"TACAS 2015","author":"M Dangl","year":"2015","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: Cpachecker with support for recursive programs and floating-point arithmetic - (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 423\u2013425. Springer, Heidelberg (2015)"},{"key":"4_CR30","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V.: Ultimate LTLAutomizer website, Feb 2015. http:\/\/ultimate.informatik.uni-freiburg.de\/ltlautomizer"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized B\u00fcchi automata. In: MASCOTS, pp. 76\u201383, IEEE (2004)","DOI":"10.1109\/MASCOT.2004.1348184"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"4_CR33","series-title":"LNCS","first-page":"455","volume-title":"TACAS 2015","author":"M Heizmann","year":"2015","unstructured":"Heizmann, M., Dietsch, D., Leike, J., Musa, B., Podelski, A.: Ultimate automizer with array interpolation - (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 455\u2013457. Springer, Heidelberg (2015)"},{"key":"4_CR34","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. 8172, pp. 365\u2013380. Springer, Heidelberg (2013)"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370, ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"4_CR38","volume-title":"The SPIN Model Checker Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker Primer and Reference Manual, vol. 1003. Addison-Wesley, Reading (2004)"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1007\/978-3-642-34026-0_45","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"F Howar","year":"2012","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 608\u2013614. Springer, Heidelberg (2012)"},{"key":"4_CR40","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)"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014)"},{"key":"4_CR42","first-page":"23","volume":"2013","author":"A Lal","year":"2013","unstructured":"Lal, A., Qadeer, S.: Reachability modulo theories. RP 2013, 23\u201344 (2013)","journal-title":"RP"},{"key":"4_CR43","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 (ETAPS). LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014)"},{"key":"4_CR44","unstructured":"McMillan, K.: Cadence SMV. Cadence Berkeley Labs, CA (2000). http:\/\/www.kenmcmil.com\/smv.html"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"4_CR46","unstructured":"McMillan, K.L.: Interpolants from Z3 proofs. In: FMCAD, pp. 19\u201327 (2011)"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-54862-8_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Ermis","year":"2014","unstructured":"Ermis, E., Nutz, A., Dietsch, D., Hoenicke, J., Podelski, A.: Ultimate kojak. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 421\u2013423. Springer, Heidelberg (2014)"},{"key":"4_CR48","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)"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341, IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL, pp. 132\u2013144, ACM (2005)","DOI":"10.1145\/1047659.1040317"},{"key":"4_CR51","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)"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-70545-1_31","volume-title":"Computer Aided Verification","author":"A Podelski","year":"2008","unstructured":"Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 314\u2013327. Springer, Heidelberg (2008)"},{"key":"4_CR53","volume-title":"Effective Correctness Criteria for Real-time Requirements","author":"AC Post","year":"2012","unstructured":"Post, A.C.: Effective Correctness Criteria for Real-time Requirements. Shaker, Aachen (2012)"},{"key":"4_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"4_CR55","series-title":"LNCS","first-page":"417","volume-title":"TACAS 2015","author":"T Str\u00f6der","year":"2015","unstructured":"Str\u00f6der, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: Aprove: termination and memory safety of C programs - (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 417\u2013419. Springer, Heidelberg (2015)"},{"key":"4_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/978-3-662-46681-0_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Urban","year":"2015","unstructured":"Urban, C.: FuncTion: an abstract domain functor for termination. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 464\u2013466. Springer, Heidelberg (2015)"},{"key":"4_CR57","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322\u2013331, IEEE Computer Society (1986)"}],"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-319-21690-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T06:28:33Z","timestamp":1748500113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}