Automated verification of termination certificates

Frédéric Blanqui 1, 2, * Kim Quyen Ly 1, 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 : In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of certificates for the termination of term rewrite systems, and formally proving its correctness in the proof assistant Coq. To this end, we use the extraction mechanism of Coq and the library on rewriting theory and termination called CoLoR.
Type de document :
Communication dans un congrès
15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam. 2012


https://hal.inria.fr/hal-00763495
Contributeur : Frédéric Blanqui <>
Soumis le : mardi 11 décembre 2012 - 04:39:30
Dernière modification le : jeudi 5 novembre 2015 - 01:06:53
Document(s) archivé(s) le : mardi 12 mars 2013 - 03:52:42

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00763495, version 1
  • ARXIV : 1212.2350

Collections

Citation

Frédéric Blanqui, Kim Quyen Ly. Automated verification of termination certificates. 15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam. 2012. <hal-00763495>

Exporter

Partager

Métriques

Consultations de
la notice

291

Téléchargements du document

108