{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:01:43Z","timestamp":1776304903786,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_11","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:00Z","timestamp":1768202520000},"page":"212-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Termination Resilience Static Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4188-7064","authenticated-orcid":false,"given":"Na\u00efm Moussaoui","family":"Remil","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8127-9642","authenticated-orcid":false,"given":"Caterina","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM (JACM), 49(5):672\u2013713 (2002)","DOI":"10.1145\/585265.585270"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Zimmermann, T., Cleland-Huang, J., Su, Z., (eds) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, pp. 326\u2013337. ACM (2016)","DOI":"10.1145\/2950290.2950351"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Nitto, E.D., Harman, M., Heymans, P., (eds) Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015, pp. 721\u2013733. ACM (2015)","DOI":"10.1145\/2786805.2786867"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T.P., (eds) Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, volume 9291 of Lecture Notes in Computer Science, pp. 145\u2013161. Springer (2015)","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Zikelic, D.: Proving non-termination by program reversal. In: Freund, S,N., Yahav, E., (eds) PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, pp. 1033\u20131048. ACM (2021)","DOI":"10.1145\/3453483.3454093"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Chen, H., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination analysis. ACM Trans. Program. Lang. Syst., 40(1):1:1\u20131:38 (2018)","DOI":"10.1145\/3121136"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Chen, Y., et al.: Advanced automata-based algorithms for program termination checking. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 135\u2013150 (2018)","DOI":"10.1145\/3192366.3192405"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Courant, N., Urban, C.: Precise widening operators for proving termination by abstract interpretation. In: Legay, A., Margaria, T., (eds) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, volume 10205 of Lecture Notes in Computer Science, pp. 136\u2013152 (2017)","DOI":"10.1007\/978-3-662-54577-5_8"},{"issue":"1\u20132","key":"11_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret. Comput. Sci. 277(1\u20132), 47\u2013103 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"11_CR10","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) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"11_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511\u2013547 (1992)","journal-title":"J. Log. Comput."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Field, J., Hicks, M., (eds) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pp. 245\u2013258. ACM (2012)","DOI":"10.1145\/2103656.2103687"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19\u201332 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: Roychoudhury, A., Cadar, C., Kim, M., (eds) Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, Singapore, Singapore, November 14-18, 2022, pp. 633\u2013645. ACM (2022)","DOI":"10.1145\/3540250.3549120"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Girol, G., Farinier, B., Bardin, S.: Not all bugs are created equal, but robust reachability can tell the difference. In: Silva, A., Rustan, K.,\u00a0Leino, M., (eds) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pp. 669\u2013693. Springer (2021)","DOI":"10.1007\/978-3-030-81685-8_32"},{"issue":"1","key":"11_CR16","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-022-00402-x","volume":"63","author":"G Girol","year":"2024","unstructured":"Girol, G., Farinier, B., Bardin, S.: Introducing robust reachability. Formal Meth. Syst. Des. 63(1), 206\u2013234 (2024)","journal-title":"Formal Meth. Syst. Des."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Hensel, J., Mensendiek, C., Giesl, J.: Aprove: non-termination witnesses for C programs - (competition contribution). In: Fisman, D., Rosu, G., (eds) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, volume 13244 of Lecture Notes in Computer Science, pp. 403\u2013407. Springer (2022)","DOI":"10.1007\/978-3-030-99527-0_21"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O., (eds) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pp. 661\u2013667. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tanahashi, K., Sato, R., Tsukada, T.: HFL(Z) validity checking for automated program verification. Proc. ACM Program. Lang., 7(POPL):154\u2013184 (2023)","DOI":"10.1145\/3571199"},{"key":"11_CR20","doi-asserted-by":"crossref","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) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pp. 779\u2013796. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Le, T.C., Antonopoulos,T., Fathololumi, P., Koskinen, E., Nguyen, T.: Dynamite: dynamic termination and non-termination proofs. Proc. ACM Program. Lang., 4(OOPSLA):189:1\u2013189:30 (2020)","DOI":"10.1145\/3428257"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: Grove, D., Blackburn, S\u00a0M., (eds) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pp. 489\u2013498. ACM (2015)","DOI":"10.1145\/2737924.2737993"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Mal\u00edk, V., Necas, F., Schrammel, P., Vojnar, T.: 2ls: arrays and loop unwinding - (competition contribution). In: Sankaranarayanan, S., Sharygina, N., (eds) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, pp. 529\u2013534. Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_31"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Metta, R., Karmarkar, H., Madhukar, K., Venkatesh, R., Chakraborty, S.: PROTON: probes for termination or not (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L., (eds ) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, volume 14572 of Lecture Notes in Computer Science, pp. 393\u2013398. Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_27"},{"key":"11_CR25","unstructured":"Remil, N. M., Urban, C., Min\u00e9, A.: Automatic detection of vulnerable variables for CTL properties of programs. In: Bj\u00f8rner, N.S., Heule, M., Voronkov, A., (eds) LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, volume 100 of EPiC Series in Computing, pp. 116\u2013126. EasyChair (2024)"},{"key":"11_CR26","unstructured":"Remil,N.M., Urban, C.: Termination resilience static analysis (artifact) (2025). https:\/\/zenodo.org\/records\/17176433"},{"key":"11_CR27","unstructured":"Parolini, F.: Static analysis for security properties of software by abstract interpretation. (Analyse statique des propri\u00e9t\u00e9s de s\u00e9curit\u00e9 des logiciels par interpr\u00e9tation abstraite) PhD thesis, Sorbonne University, Paris, France (2024)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Parolini, F., Min\u00e9, A.: Sound abstract nonexploitability analysis. In: Dimitrova, R., Lahav, O., Wolff, S., (eds) Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II, volume 14500 of Lecture Notes in Computer Science, pp. 314\u2013337. Springer (2024)","DOI":"10.1007\/978-3-031-50521-8_15"},{"issue":"OOPSLA2","key":"11_CR29","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1145\/3689720","volume":"8","author":"A Raad","year":"2024","unstructured":"Raad, A., Vanegue, J., O\u2019Hearn, P.W.: Non-termination proving at scale. Proc. ACM Program. Lang. 8(OOPSLA2), 246\u2013274 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Shi, X., et al.: Large-scale analysis of non-termination bugs in real-world OSS projects. In: Roychoudhury, A., Cadar, C., Kim, M., eds, Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, Singapore, Singapore, November 14-18, 2022, pp. 256\u2013268. ACM (2022)","DOI":"10.1145\/3540250.3549129"},{"key":"11_CR31","unstructured":"Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369 (1949)"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Urban, C.: FuncTion: an abstract domain functor for termination - (competition contribution). In: Baier, C., Tinelli, C., (eds) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9035 of Lecture Notes in Computer Science, pp. 464\u2013466. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"11_CR33","unstructured":"Urban, C.: Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs (Analyse Statique par Interpr\u00e9tation Abstraite de Propri\u00e9t\u00e9s Temporelles Fonctionnelles des Programmes). PhD thesis, \u00c9cole Normale Sup\u00e9rieure, Paris, France (2015)"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H., (eds)Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, volume 8723 of Lecture Notes in Computer Science, pp. 302\u2013318. Springer (2014)","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"11_CR35","unstructured":"Urban, C., Min\u00e9, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z., (eds) Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pp. 412\u2013431. Springer (2014)"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Urban, C., Ueltschi, S., M\u00fcller, P.: Abstract interpretation of CTL properties. In: Podelski, A., (eds) Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, volume 11002 of Lecture Notes in Computer Science, pp. 402\u2013422. Springer (2018)","DOI":"10.1007\/978-3-319-99725-4_24"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Zhang, Y., et al.: Endwatch: a practical method for detecting non-termination in real-world software. In: 2023 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 686\u2013697. IEEE (2023)","DOI":"10.1109\/ASE56229.2023.00061"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:22:08Z","timestamp":1768202528000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}