Automated Verification of Termination Certificates
Source: Cornell University
In order to increase user confidence, many automated theorem proverbs provide certificates that can be independently verified. In this paper, the authors report on their 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, they use the extraction mechanism of Coq and the library on rewriting theory and termination called Color. Being able to prove the correctness of a program is important, especially for critical applications (banking, aeronautics, etc). But this is generally undesirable. So, many different and complementary approaches have been developed for tackling this problem: software engineering methodologies, testing, model-checking, formal proof, etc.