The Certification Problem Format
Christian Sternagel (University of Innsbruck, Austria), Ren\'e, Thiemann (University of Innsbruck, Austria)
TL;DR
The paper presents CPF, a versatile format for certifying various properties of term rewrite systems, supported by tools and used in international competitions for verification tasks.
Contribution
It introduces CPF as a unified format for multiple proof types, enhancing interoperability and trust in automated verification tools.
Findings
CPF supports proofs for termination, confluence, complexity, and completion.
CPF is adopted by several tools and certifiers.
CPF is used in international competitions for verification exchange.
Abstract
We provide an overview of CPF, the certification problem format, and explain some design decisions. Whereas CPF was originally invented to combine three different formats for termination proofs into a single one, in the meanwhile proofs for several other properties of term rewrite systems are also expressible: like confluence, complexity, and completion. As a consequence, the format is already supported by several tools and certifiers. Its acceptance is also demonstrated in international competitions: the certified tracks of both the termination and the confluence competition utilized CPF as exchange format between automated tools and trusted certifiers.
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.