Automated verification of termination certificates
Logic in Computer Science
2012-12-12 v1 Mathematical Software
Software Engineering
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.
Keywords
Cite
@article{arxiv.1212.2350,
title = {Automated verification of termination certificates},
author = {Frédéric Blanqui and Kim Quyen Ly},
journal= {arXiv preprint arXiv:1212.2350},
year = {2012}
}