{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:40:24Z","timestamp":1758667224624,"version":"3.44.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,25]],"date-time":"2025-08-25T00:00:00Z","timestamp":1756080000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,25]],"date-time":"2025-08-25T00:00:00Z","timestamp":1756080000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005714","name":"Technische Universit\u00e4t Darmstadt","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005714","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We consider automated reasoning about recursively defined partial functions with decidable domain, i.e. functions computed by incompletely defined (or underspecified) but terminating functional programs. We define an interpreter for those programs, consider termination and investigate the semantics of incompletely defined programs. The interpreter may halt with a stuck computation, e.g. when dividing a number by zero, which represents a runtime error in a conventional programming environment. We show how so-called domain procedures are synthesized which decide the domain of incompletely defined procedures in almost all cases. As calls of domain procedures occur in proof obligations, domain procedures are optimized to make them as simple as possible. We also use domain procedures to refine the program semantics such that statements causing stuck computations do not hold. Our method to reason about incompletely defined programs is implemented in the verification tool .<\/jats:p>","DOI":"10.1007\/s10817-025-09722-z","type":"journal-article","created":{"date-parts":[[2025,8,25]],"date-time":"2025-08-25T06:06:21Z","timestamp":1756101981000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning About Incompletely Defined Programs"],"prefix":"10.1007","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9382-5399","authenticated-orcid":false,"given":"Christoph","family":"Walther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,25]]},"reference":[{"key":"9722_CR1","unstructured":"Aderhold, M., Walther, C., Szallies, D., Schlosser, A.: A fast disprover for $$\\checkmark $$eriFun. In: Ahrendt, W., Baumgartner, P., de Nivelle, H. (eds.) Proceedings of Workshop on Non-theorems, Non-validity, Non-provability (DISPROVING-06), 2006, Seattle, WA, pp. 59\u201369 (2006). http:\/\/verifun.de\/documents"},{"key":"9722_CR2","unstructured":"Arthan, R.D.: Undefinedness in Z: issues for specification and proof. In: Proceedings of CADE 13 Workshop on Mechanization of Partial Functions, 1996 (1996). http:\/\/www.cs.bham.ac.uk\/$$\\sim $$mmk\/cade96-partiality\/"},{"key":"9722_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"issue":"4","key":"9722_CR4","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10817-011-9236-z","volume":"47","author":"H de Nivelle","year":"2011","unstructured":"de Nivelle, H.: Classical logic with partial functions. J. Autom. Reason. 47(4), 399\u2013425 (2011). https:\/\/doi.org\/10.1007\/s10817-011-9236-z","journal-title":"J. Autom. Reason."},{"key":"9722_CR5","unstructured":"Farmer, W.M.: Mechanizing the traditional approach to partial functions. In: Proceedings of CADE 13 Workshop on Mechanization of Partial Functions, 1996 (1996). http:\/\/www.cs.bham.ac.uk\/$$\\sim $$mmk\/cade96-partiality\/"},{"key":"9722_CR6","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems, pp. 125\u2013128. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"9722_CR7","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1023\/A:1005702928286","volume":"18","author":"S Finn","year":"1997","unstructured":"Finn, S., Fourmann, M.P., Longley, J.: Partial functions in a total setting. J. Autom. Reason. 18, 85\u2013104 (1997). https:\/\/doi.org\/10.1023\/A:1005702928286","journal-title":"J. Autom. Reason."},{"key":"9722_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1006408829523","volume":"26","author":"J Giesl","year":"2001","unstructured":"Giesl, J.: Induction proofs with partial functions. J. Autom. Reason. 26, 1\u201349 (2001). https:\/\/doi.org\/10.1023\/A:1006408829523","journal-title":"J. Autom. Reason."},{"key":"9722_CR9","doi-asserted-by":"publisher","unstructured":"Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In: van Leeuwen, J. (ed.) Computer Science Today: Recent Trends and Developments. Lecture Notes in Computer Science, vol. 1000, pp. 366\u2013373. Springer (1995). https:\/\/doi.org\/10.1007\/BFb0015254","DOI":"10.1007\/BFb0015254"},{"issue":"4","key":"9722_CR10","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1093\/jigpal\/jzi032","volume":"13","author":"R H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415\u2013433 (2005). https:\/\/doi.org\/10.1093\/jigpal\/jzi032","journal-title":"Log. J. IGPL"},{"key":"9722_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00042-B","author":"CB Jones","year":"1995","unstructured":"Jones, C.B.: Partial functions and logics: a warning. Inf. Process. Lett. (1995). https:\/\/doi.org\/10.1016\/0020-0190(95)00042-B","journal-title":"Inf. Process. Lett."},{"key":"9722_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.10.002","volume":"145","author":"CB Jones","year":"2006","unstructured":"Jones, C.B.: Reasoning about partial functions in the formal development of programs. Electron. Notes Theor. Comput. Sci. 145, 3\u201325 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.10.002","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9722_CR13","unstructured":"Kapur, D., Musser, D.R.: Inductive reasoning with incomplete specifications. In: Symposium on Logic in Computer Science, 1986, vol. 720, pp. 367\u2013377. IEEE Computer Society, Cambridge (1986)"},{"key":"9722_CR14","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Bibliotheca Mathematica. North Holland, Amsterdam (1952)"},{"issue":"4","key":"9722_CR15","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303\u2013336 (2010). https:\/\/doi.org\/10.1007\/s10817-009-9157-2","journal-title":"J. Autom. Reason."},{"key":"9722_CR16","doi-asserted-by":"publisher","unstructured":"Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J.R., Padon, O., Parno, B.: Verus: a practical foundation for systems verification. In: Proceedings of ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024, Austin, TX, USA, pp. 438\u2013454 (2024). https:\/\/doi.org\/10.1145\/3694715.3695952","DOI":"10.1145\/3694715.3695952"},{"key":"9722_CR17","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348\u2013370. Springer, Dakar (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"9722_CR18","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P Manolios","year":"2003","unstructured":"Manolios, P., Moore, J.S.: Partial functions in ACL2. J. Autom. Reason. 31, 107\u2013127 (2003). https:\/\/doi.org\/10.1023\/B:JARS.0000009505.07087.34","journal-title":"J. Autom. Reason."},{"key":"9722_CR19","doi-asserted-by":"publisher","unstructured":"Mehta, F.: A practical approach to partiality\u2014a proof based approach. In: Formal Methods and Software Engineering, 10th International Conference on Formal Engineering Methods, ICFEM 2008. Lecture Notes in Computer Science, 2008, vol. 5256, pp. 238\u2013257. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_16","DOI":"10.1007\/978-3-540-88194-0_16"},{"key":"9722_CR20","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"issue":"9","key":"9722_CR21","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"JM Rushby","year":"1998","unstructured":"Rushby, J.M., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998). https:\/\/doi.org\/10.1109\/32.713327","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"9722_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1093\/comjnl\/42.2.73","volume":"42","author":"B Schieder","year":"1999","unstructured":"Schieder, B., Broy, M.: Adapting calculational logic to the undefined. Comput. J. 42(2), 73\u201381 (1999). https:\/\/doi.org\/10.1093\/comjnl\/42.2.73","journal-title":"Comput. J."},{"issue":"7","key":"9722_CR23","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.10.038","volume":"174","author":"A Schlosser","year":"2007","unstructured":"Schlosser, A., Walther, C., Gonder, M., Aderhold, M.: Context dependent procedures and computed types in $$\\checkmark $$eriFun. Electron. Notes Theor. Comput. Sci. 174(7), 61\u201378 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2006.10.038","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9722_CR24","doi-asserted-by":"publisher","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoue, J.-K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: Proceedings of 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, St. Petersburg, FL, USA, pp. 256\u2013270 (2016). https:\/\/doi.org\/10.1145\/2914770.2837655","DOI":"10.1145\/2914770.2837655"},{"key":"9722_CR25","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: Proceedings of 19th ACM SIGPLAN International Conference on Functional Programming, 2014, pp. 269\u2013282 (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"9722_CR26","unstructured":"VeriFun. http:\/\/www.verifun.de"},{"issue":"1","key":"9722_CR27","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C Walther","year":"1994","unstructured":"Walther, C.: On proving the termination of algorithms by machine. Artif. Intell. 71(1), 101\u2013157 (1994). https:\/\/doi.org\/10.1016\/0004-3702(94)90063-9","journal-title":"Artif. Intell."},{"key":"9722_CR28","doi-asserted-by":"publisher","unstructured":"Walther, C., Schweitzer, S.: Verification in the classroom. J. Autom. Reason. Spec. Issue Autom. Reason. Theorem Proving Educ. 32(1), 35\u201373 (2004). https:\/\/doi.org\/10.1023\/B:JARS.0000021872.64036.41","DOI":"10.1023\/B:JARS.0000021872.64036.41"},{"key":"9722_CR29","doi-asserted-by":"publisher","unstructured":"Walther, C., Schweitzer, S.: Automated termination analysis for incompletely defined programs. In: Baader, F., Voronkov, A. (eds.) Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-11). Lecture Notes in Artificial Intelligence, 2005, vol. 3452, pp. 332\u2013346. Springer, Montevideo (2005). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_22","DOI":"10.1007\/978-3-540-32275-7_22"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09722-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09722-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09722-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:29Z","timestamp":1758664949000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09722-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,25]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9722"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09722-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,8,25]]},"assertion":[{"value":"29 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no Conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"25"}}