Skip to Main content Skip to Navigation
New interface
Conference papers

Automated verification of termination certificates

Frédéric Blanqui 1, 2, * Kim Quyen Ly 1, 2 
* Corresponding author
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.
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Tuesday, December 11, 2012 - 4:39:30 AM
Last modification on : Thursday, February 3, 2022 - 11:16:57 AM
Long-term archiving on: : Tuesday, March 12, 2013 - 3:52:42 AM


Files produced by the author(s)


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



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



Record views


Files downloads