| Automated Verification of Certificates for Termination Proofs |  |
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 verication of the results of such automated termination provers. This
is accomplished by means of termination certicates, that can be easily generated by termination provers, and then by the
transformation of those certicates 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 certicates into termination proofs veriable by Coq.
Automated Verification of Certificates for Termination Proofs INRIA Research Report 6949, INRIA, Paris, France, June 2009 BibTeX:@techreport{color-TR-09,
author = {Fr\'ed\'eric Blanqui and Adam Koprowski},
title = {Automated Verification of Certificates for Termination Proofs},
year = {2009},
month = {June},
institution = {INRIA},
address = {Paris, France},
number = {6949},
} | 
