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 de-
cision 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.

Certifying Proofs in the First-Order Theory of Rewriting

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme