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.
