License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.27
URN: urn:nbn:de:0030-drops-139228
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13922/
Go to the corresponding LIPIcs Volume Portal

Muñoz, Cesar A. ; Ayala-Rincón, Mauricio ; Moscato, Mariano M. ; Dutle, Aaron M. ; Narkawicz, Anthony J. ; Almeida, Ariane A. ; Avelar, Andréia B. ; M. Ferreira Ramos, Thiago

Formal Verification of Termination Criteria for First-Order Recursive Functions

pdf-format:
LIPIcs-ITP-2021-27.pdf (0.9 MB)

Abstract

This paper presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs.

BibTeX - Entry

@InProceedings{munoz_et_al:LIPIcs.ITP.2021.27,
  author =	{Mu\~{n}oz, Cesar A. and Ayala-Rinc\'{o}n, Mauricio and Moscato, Mariano M. and Dutle, Aaron M. and Narkawicz, Anthony J. and Almeida, Ariane A. and Avelar, Andr\'{e}ia B. and M. Ferreira Ramos, Thiago},
  title =	{{Formal Verification of Termination Criteria for First-Order Recursive Functions}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13922},
  URN =		{urn:nbn:de:0030-drops-139228},
  doi =		{10.4230/LIPIcs.ITP.2021.27},
  annote =	{Keywords: Formal Verification, Termination, Calling Context Graph, PVS}
}

Keywords: Formal Verification, Termination, Calling Context Graph, PVS
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Other (NASA PVS Library): https://github.com/nasa/pvslib

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI