Automated verification of termination certificates

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.
Document type :
Conference papers
15th National Symposium of Selected ICT Problems, Dec 2012, Hanoi, Vietnam. 2012


https://hal.inria.fr/hal-00763495
Contributor : Frédéric Blanqui <>
Submitted on : Tuesday, December 11, 2012 - 4:39:30 AM
Last modification on : Tuesday, December 11, 2012 - 10:24:50 AM

Files

main.pdf
fileSource_public_author

Identifiers

  • 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>

Export

Share

Metrics

Consultation de
la notice

200

Téléchargement du document

43