Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer
27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), LNCS 12652, pp. 127 – 144, 2021.
pdf 
doi:10.1007/978-3-030-72013-1_7
Abstract
The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify.
BibTex
@inproceedings{MLMF-TACAS21, author = "Fabian Mitterwallner and Alexander Lochmann and Aart Middeldorp and Bertram Felgenhauer", title = "Certifying Proofs in the First-Order Theory of Rewriting", booktitle = "Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Jan Friso Groote and Kim Guldstrand Larsen", series = "Lecture Notes in Computer Science", volume = 12652, pages = "127--144", year = 2021, doi = "10.1007/978-3-030-72013-1_7"}