A Framework for Developing Stand-Alone Certifiers

Christian Sternagel and René Thiemann

Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014), Electronic Notes in Theoretical Computer Science 312, pp. 51 – 67, 2015.


Current tools for automated deduction are often powerful and complex. Due to their complexity there is a risk that they contain bugs and thus deliver wrong results. To ensure reliability of these tools, one possibility is to develop certifiers which check the results of tools with the help of a trusted proof assistant. We present a framework which illustrates the essential steps to develop stand-alone certifiers which efficiently check generated proofs outside the employed proof assistant. Our framework has already been used to develop certifiers for various properties, including termination, confluence, completion, and tree automata related properties.


  PDF |    doi:10.1016/j.entcs.2015.04.004  |  © Creative Commons License – NC – ND


author = "Christian Sternagel and Ren\'e Thiemann",
title = "A Framework for Developing Stand-Alone Certifiers",
booktitle = "Proceedings of the 9th Workshop on
on Logical and Semantic Frameworks, with Applications",
journal = "Electronic Notes in Theoretical Computer Science",
volume = 312,
pages = "51--67",
year = 2015,
doi = "10.1016/j.entcs.2015.04.004"
Nach oben scrollen