| 2021 | CPP | 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 |
| 2021 | TACAS | Certifying Proofs in the First-Order Theory of Rewriting. | Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer |
| 2019 | CPP | A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. | Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp |
| 2018 | ICTAC | Layer Systems for Confluence - Formalized. | Bertram Felgenhauer, Franziska Rapp |
| 2017 | CADE | Beyond DRAT: Challenges in Certifying UNSAT. | Bertram Felgenhauer |
| 2017 | CADE | CSI: New Evidence - A Progress Report. | Julian Nagele, Bertram Felgenhauer, Aart Middeldorp |
| 2017 | ICTAC | Constructing Cycles in the Simplex Method for DPLL(T). | Bertram Felgenhauer, Aart Middeldorp |
| 2014 | LATA | Reachability Analysis with State-Compatible Automata. | Bertram Felgenhauer, Ren Thiemann |
| 2011 | CADE | CSI - A Confluence Tool. | Harald Zankl, Bertram Felgenhauer, Aart Middeldorp |