Automated Verification of Termination Certificates

Frédéric Blanqui 1, * Adam Koprowski 2
* Auteur correspondant
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : Termination is an important property required for total correctness of programs/algorithms. In particular it is a well studied subject in the area of term rewriting, where a number of methods and tools for proving termination has been developed over the years. Ensuring reliability of those tools is an important and challenging issue. In this paper we present a methodology and a tool for the automated verification of the results of such automated termination provers. This is accomplished by means of termination certificates, that can be easily generated by termination provers, and then by the transformation of those certificates into full formal proofs in some proof assistant/checker. This last step is done by formalizing the proofs of termination criteria used in modern termination provers. In this paper we describe the formalization of some of these criteria in the proof assistant Coq and the application of those formalizations in the transformation of termination certificates into termination proofs verifiable by Coq.
Type de document :
Rapport
[Research Report] RR-6949, INRIA. 2009, pp.24
Liste complète des métadonnées

Littérature citée [5 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00390902
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 3 juin 2009 - 08:33:24
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : lundi 15 octobre 2012 - 11:40:36

Fichier

RR-6949.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00390902, version 1

Collections

Citation

Frédéric Blanqui, Adam Koprowski. Automated Verification of Termination Certificates. [Research Report] RR-6949, INRIA. 2009, pp.24. 〈inria-00390902〉

Partager

Métriques

Consultations de la notice

359

Téléchargements de fichiers

98