cl-banner

Certifying Proofs in the First-Order Theory of Rewriting

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

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.

 

  PDF |    doi:10.1007/978-3-030-72013-1_7

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"
}
Nach oben scrollen