CSI - A Confluence Tool. - Harald Zankl; Bertram Felgenhauer; Aart Middeldorp (CADE, 2011)

Layer Systems for Proving Confluence. - Bertram Felgenhauer; Harald Zankl; Aart Middeldorp (FSTTCS, 2011)

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time. - Bertram Felgenhauer (RTA, 2012)

Proof Orders for Decreasing Diagrams. - Bertram Felgenhauer; Vincent van Oostrom (RTA, 2013)

A Haskell Library for Term Rewriting. - Bertram Felgenhauer; Martin Avanzini; Christian Sternagel (CoRR, 2013)

Reachability Analysis with State-Compatible Automata. - Bertram Felgenhauer; René Thiemann (LATA, 2014)

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. - Julian Nagele; Bertram Felgenhauer; Aart Middeldorp (RTA, 2015)

Decreasing Diagrams II. - Bertram Felgenhauer (Arch. Formal Proofs, 2015)

Labelings for Decreasing Diagrams. - Harald Zankl; Bertram Felgenhauer; Aart Middeldorp (J. Autom. Reason., 2015)

Layer Systems for Proving Confluence. - Bertram Felgenhauer; Aart Middeldorp; Harald Zankl; Vincent van Oostrom (ACM Trans. Comput. Log., 2015)

The Z Property. - Bertram Felgenhauer; Julian Nagele; Vincent van Oostrom; Christian Sternagel (Arch. Formal Proofs, 2016)

Beyond DRAT: Challenges in Certifying UNSAT. - Bertram Felgenhauer (ARCADE@CADE, 2017)

CSI: New Evidence - A Progress Report. - Julian Nagele; Bertram Felgenhauer; Aart Middeldorp (CADE, 2017)

Constructing Cycles in the Simplex Method for DPLL(T). - Bertram Felgenhauer; Aart Middeldorp (ICTAC, 2017)

Reachability, confluence, and termination analysis with state-compatible automata. - Bertram Felgenhauer; René Thiemann (Inf. Comput., 2017)

Certifying Confluence Proofs via Relative Termination and Rule Labeling. - Julian Nagele; Bertram Felgenhauer; Harald Zankl (Log. Methods Comput. Sci., 2017)

Layer Systems for Confluence - Formalized. - Bertram Felgenhauer; Franziska Rapp (ICTAC, 2018)

Minsky Machines. - Bertram Felgenhauer (Arch. Formal Proofs, 2018)

Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently. - Bertram Felgenhauer (Log. Methods Comput. Sci., 2018)

A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. - Bertram Felgenhauer; Aart Middeldorp; T. V. H. Prathamesh; Franziska Rapp (CPP, 2019)

Implementing the Goodstein Function in λ-Calculus. - Bertram Felgenhauer (Arch. Formal Proofs, 2020)

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. - Alexander Lochmann; Aart Middeldorp; Fabian Mitterwallner; Bertram Felgenhauer (CPP, 2021)

Certifying Proofs in the First-Order Theory of Rewriting. - Fabian Mitterwallner; Alexander Lochmann; Aart Middeldorp; Bertram Felgenhauer (TACAS (2), 2021)

Regular Tree Relations. - Alexander Lochmann; Bertram Felgenhauer; Christian Sternagel; René Thiemann; Thomas Sternagel (Arch. Formal Proofs, 2021)

First-Order Theory of Rewriting. - Alexander Lochmann; Bertram Felgenhauer (Arch. Formal Proofs, 2022)

First-Order Rewriting. - René Thiemann; Christian Sternagel; Christina Kirk; Martin Avanzini; Bertram Felgenhauer; Julian Nagele; Thomas Sternagel; Sarah Winkler; Akihisa Yamada 002 (Arch. Formal Proofs, 2025)