Formal verification of termination criteria for first-order recursive functions

DOI10.1007/S10817-023-09669-ZMaRDI QIDQ6149593zbMATH OpenOpenAlexFDO

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

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

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 2043534 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 7699444 (Why is no real title available?)
• An axiomatic basis for computer programming
• Certified Size-Change Termination
• Enumeration of the Elementary Circuits of a Directed Graph
• Formalization of the computational theory of a Turing complete functional language model
• Formalization of the undecidability of the halting problem for a functional language
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Introduction to algorithms.
• Termination Analysis with Calling Context Graphs
• Termination of Isabelle functions via termination of rewriting
• The size-change principle and dependency pairs for termination of term rewriting
• The size-change principle for program termination

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6149593)