Automated verification of termination certificates
Fr\'ed\'eric Blanqui (LIAMA, LCS), Kim Quyen Ly (LIAMA, LCS)
TL;DR
This paper presents a verified standalone tool for checking termination certificates of term rewrite systems, leveraging Coq's extraction mechanism and the CoLoR library to ensure correctness.
Contribution
It introduces a formally verified tool for termination certificate verification, combining Coq's proof assistant capabilities with rewriting theory.
Findings
Successfully developed a verified termination certificate checker
Proved the correctness of the checker within Coq
Utilized Coq's extraction mechanism and CoLoR library
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Security and Verification in Computing · Formal Methods in Verification