6th International School on Rewriting >> Certification of Rewriting Properties

6th International School on Rewriting

July 16th - 20th, 2012. Valencia, Spain

CER: Certification of Rewriting Properties

The purpose of this course is to give an overview on different techniques and approaches to the certification of proofs.

Various automated techniques for rewriting systems (termination proofs, confluence proofs, completion, etc.) involve software that is of big size and high complexity, thus prone to bugs. As a matter of fact, almost all automated provers have exhibited incorrect behaviours at some stage, and the certification of their results has become an important topic. We will discuss several issues regarding techniques to make an automated prover trustworthy, depending on the end-use of them, and point out a few pitfalls to be avoided.

<< Back to Previous Page.