{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:21Z","timestamp":1740123261997,"version":"3.37.3"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,11,29]],"date-time":"2023-11-29T00:00:00Z","timestamp":1701216000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,11,29]],"date-time":"2023-11-29T00:00:00Z","timestamp":1701216000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"NASA\/NIA","award":["NNL09AA00A"],"award-info":[{"award-number":["NNL09AA00A"]}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["409003\/21-2, RG 313290\/21-0"],"award-info":[{"award-number":["409003\/21-2, RG 313290\/21-0"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005668","name":"Funda\u00e7\u00e3o de Apoio \u00e1 Pesquisa do Distrito Federal","doi-asserted-by":"publisher","award":["00193.00001175\/21-11"],"award-info":[{"award-number":["00193.00001175\/21-11"]}],"id":[{"id":"10.13039\/501100005668","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s10817-023-09669-z","type":"journal-article","created":{"date-parts":[[2023,11,29]],"date-time":"2023-11-29T03:02:02Z","timestamp":1701226922000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of Termination Criteria for First-Order Recursive Functions"],"prefix":"10.1007","volume":"67","author":[{"given":"Cesar A.","family":"Mu\u00f1oz","sequence":"first","affiliation":[]},{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6468-9498","authenticated-orcid":false,"given":"Mariano M.","family":"Moscato","sequence":"additional","affiliation":[]},{"given":"Aaron M.","family":"Dutle","sequence":"additional","affiliation":[]},{"given":"Anthony J.","family":"Narkawicz","sequence":"additional","affiliation":[]},{"given":"Ariane Alves","family":"Almeida","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9ia B. Avelar","family":"da Silva","sequence":"additional","affiliation":[]},{"given":"Thiago M. Ferreira","family":"Ramos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,29]]},"reference":[{"key":"9669_CR1","unstructured":"Abel, A.: foetus\u2014Termination Checker for Simple Functional Programs. Programming Lab Report 474, LMU M\u00fcnchen (1998). http:\/\/www.cse.chalmers.se\/~abela\/foetus\/"},{"key":"9669_CR2","unstructured":"Alves\u00a0Almeida, A.: On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS. Ph.D. thesis, Universidade de Bras\u00edlia, Graduate Program in Informatics, Bras\u00edlia, Distrito Federal, Brazil (2021). https:\/\/repositorio.unb.br\/handle\/10482\/42296"},{"key":"9669_CR3","doi-asserted-by":"publisher","first-page":"102474","DOI":"10.1016\/j.scico.2020.102474","volume":"195","author":"A Alves Almeida","year":"2020","unstructured":"Alves Almeida, A., Ayala-Rinc\u00f3n, M.: Formalizing the dependency pair criterion for innermost termination. Sci. Comput. Program. 195, 102474 (2020). https:\/\/doi.org\/10.1016\/j.scico.2020.102474","journal-title":"Sci. Comput. Program."},{"key":"9669_CR4","unstructured":"Avelar, A.B.: Formaliza\u00e7\u00e3o da automa\u00e7\u00e3o da termina\u00e7\u00e3o atrav\u00e9s de grafos com matrizes de medida. Ph.D. thesis, Universidade de Bras\u00edlia, Departamento de Matem\u00e1tica, Bras\u00edlia, Distrito Federal, Brazil (2015). https:\/\/repositorio.unb.br\/handle\/10482\/18069. (In Portuguese)"},{"key":"9669_CR5","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. Springer-Verlag Berlin Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9669_CR6","volume-title":"A Computational Logic","author":"RS Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, Cambridge (1979)"},{"key":"9669_CR7","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"},{"key":"9669_CR8","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."},{"issue":"10","key":"9669_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"9669_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, New York (2000)"},{"key":"9669_CR11","doi-asserted-by":"publisher","unstructured":"Krauss, A.: Certified Size-Change Termination. In: Automated Deduction\u2014CADE-21, 21st International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 4603, pp. 460\u2013475. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_34","DOI":"10.1007\/978-3-540-73595-3_34"},{"key":"9669_CR12","doi-asserted-by":"publisher","unstructured":"Krauss, A., Sternagel, C., Thiemann, R., Fuhs, C., Giesl, J.: Termination of Isabelle Functions via Termination of Rewriting. In: Interactive Theorem Proving - Second International Conference, ITP 2011, Lecture Notes in Computer Science, vol. 6898, pp. 152\u2013167. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_13","DOI":"10.1007\/978-3-642-22863-6_13"},{"key":"9669_CR13","doi-asserted-by":"publisher","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81\u201392 (2001). https:\/\/doi.org\/10.1145\/360204.360210","DOI":"10.1145\/360204.360210"},{"key":"9669_CR14","doi-asserted-by":"publisher","unstructured":"Manolios, P., Vroon, D.: Termination Analysis with Calling Context Graphs. In: Computer Aided Verification, 18th International Conference, CAV, Lecture Notes in Computer Science, vol. 4144, pp. 401\u2013414. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_36","DOI":"10.1007\/11817963_36"},{"key":"9669_CR15","unstructured":"Mu\u00f1oz, C.A., Ayala-Rinc\u00f3n, M., Moscato, M.M., Dutle, A.M., Narkawicz, A.J., Almeida, A.A., Avelar, A.B., M.\u00a0Ferreira\u00a0Ramos, T.: Formal Verification of Termination Criteria for First-Order Recursive Functions. In: L.\u00a0Cohen, C.\u00a0Kaliszyk (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021), Leibniz International Proceedings in Informatics (LIPIcs), vol. 193, pp. 27:1\u201327:17. Schloss Dagstuhl\u2013Leibniz\u2013Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). 10.4230\/LIPIcs.ITP.2021.27. https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13922"},{"key":"9669_CR16","doi-asserted-by":"publisher","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 607, pp. 748\u2013752. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"4","key":"9669_CR17","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1007\/s10817-021-09615-x","volume":"66","author":"TMF Ramos","year":"2022","unstructured":"Ramos, T.M.F., Alves Almeida, A., Ayala-Rinc\u00f3n, M.: Formalization of the computational theory of a turing complete functional language model. J. Autom. Reason. 66(4), 1031\u20131063 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09615-x","journal-title":"J. Autom. Reason."},{"key":"9669_CR18","doi-asserted-by":"publisher","unstructured":"Ramos, T.M.F., Mu\u00f1oz, C., Ayala-Rinc\u00f3n, M., Moscato, M., Dutle, A., Narkawicz, A.: Formalization of the Undecidability of the Halting Problem for a Functional Language. In: Logic, Language, Information, and Computation, Lecture Notes in Computer Science, vol. 10944, pp. 196\u2013209. Springer Berlin Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-57669-4_11","DOI":"10.1007\/978-3-662-57669-4_11"},{"issue":"3","key":"9669_CR19","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1137\/0202017","volume":"2","author":"R Tarjan","year":"1973","unstructured":"Tarjan, R.: Enumeration of the elementary circuits of a directed graph. SIAM J. Comput. 2(3), 211\u2013216 (1973)","journal-title":"SIAM J. Comput."},{"key":"9669_CR20","doi-asserted-by":"publisher","unstructured":"Thiemann, R., Giesl, J.: Size-Change Termination for Term Rewriting. In: Proceedings Rewriting Techniques and Applications, 14th International Conference, RTA, Lecture Notes in Computer Science, vol. 2706, pp. 264\u2013278. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44881-0_19","DOI":"10.1007\/3-540-44881-0_19"},{"issue":"4","key":"9669_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput. 16(4), 229\u2013270 (2005). https:\/\/doi.org\/10.1007\/s00200-005-0179-7","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"1","key":"9669_CR22","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"A Turing","year":"1937","unstructured":"Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42(1), 230\u2013265 (1937)","journal-title":"Proc. Lond. Math. Soc."},{"key":"9669_CR23","unstructured":"Turing, A.: Checking a large routine. In: Report of a Conference High Speed Automatic Calculating-Machines, pp. 67\u201369. University Mathematical Laboratory (1949)"},{"key":"9669_CR24","unstructured":"Vroon, D.: Automatically proving the termination of functional programs. Ph.D. thesis, Georgia Institute of Technology (2007)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09669-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09669-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09669-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,9]],"date-time":"2023-12-09T09:05:41Z","timestamp":1702112741000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09669-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,29]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9669"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09669-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,11,29]]},"assertion":[{"value":"10 September 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 April 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 November 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"40"}}