Formal verification of termination criteria for first-order recursive functions

DOI10.1007/s10817-023-09669-zOpenAlexW3174648313MaRDI QIDQ6149593

Andréia B. Avelar da Silva, Ariane Alves Almeida, Mariano M. Moscato, César A. Muñoz, Anthony Narkawicz, Thiago Mendonça Ferreira Ramos, Unnamed Author, Mauricio Ayala-Rincón

Publication date: 6 February 2024

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-023-09669-z

zbMATH Keywords

formal verificationterminationPVScalling context graph

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Formalization of the undecidability of the halting problem for a functional language
• Formalization of the computational theory of a Turing complete functional language model
• The size-change principle and dependency pairs for termination of term rewriting
• Termination of Isabelle Functions via Termination of Rewriting
• Certified Size-Change Termination
• The size-change principle for program termination
• Enumeration of the Elementary Circuits of a Directed Graph
• An axiomatic basis for computer programming
• Termination Analysis with Calling Context Graphs

This page was built for publication: Formal verification of termination criteria for first-order recursive functions