Journal Publications
-
Bertram Felgenhauer
Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
Logical Methods in Computer Science 14(4:7), pp. 1–35, 2018
doi: 10.23638/LMCS-14(4:7)2018
-
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Logical Methods in Computer Science 13(2:4), pp. 1–27, 2017
doi: 10.23638/LMCS-13(2:4)2017
-
Bertram Felgenhauer and René Thiemann
Reachability, confluence, and termination analysis with state-compatible automata
Information and Computation 253(3), pp. 467–483, 2017
doi: 10.1016/j.ic.2016.06.011
-
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, and Vincent van Oostrom
Layer Systems for Proving Confluence (preprint looks nicer)
ACM Transactions on Computational Logic 16(2:14), pp. 1–32, 2015.
doi: 10.1145/2710017
-
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Labelings for Decreasing Diagrams
Journal of Automated Reasoning 54(2), pp. 101–133, 2015.
doi: 10.1007/s10817-014-9316-y
Publications in Proceedings
-
Bertram Felgenhauer, Aart Middeldorp, T.V.H. Prathamesh, and Franziska Rapp
A Verified Ground Confluence Tool for Linear Variable-Separated Rewrite Systems in Isabelle/HOL
In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019),
ACM, New York, pp. 132–143, 2019.
CC BY-ND 4.0
doi: 10.1145/3293880.3294098
-
Bertram Felgenhauer and Franziska Rapp
Layer Systems for Confluence—Formalized
In Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018),
Lecture Notes in Computer Science 11187, pp. 173–190, 2018.
CC BY 4.0
doi: 10.1007/978-3-030-02508-3_10
-
Bertram Felgenhauer and Aart Middeldorp
Constructing Cycles in the Simplex Method for DPLL(T)
In Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017),
Lecture Notes in Computer Science 10580, pp. 213–228, 2017.
© Springer
doi: 10.1007/978-3-319-67729-3_13
-
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
CSI: New Evidence — A Progress Report
In Proceedings of the 26th International Conference on Automated Deduction (CADE-26),
Lecture Notes in Artificial Intelligence 10395, pp. 385–397, 2017.
© Springer
doi: 10.1007/978-3-319-63046-5_24
-
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Improving Automated Confluence Analysis of Rewrite Systems by Redundant Rules
In Proceedings of the 26th International Confluence on Rewriting Techniques and Automation (RTA 2015),
Leibniz International Proceedings in Informatics 36, pp. 257–268, 2015.
doi: 10.4230/LIPIcs.RTA.2015.257
-
Bertram Felgenhauer and René Thiemann
Reachability Analysis with State-Compatible Automata
In Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014),
Lecture Notes in Computer Science 8370, pp. 347–359, 2014.
© Springer
doi: 10.1007/978-3-319-04921-2_28
-
Bertram Felgenhauer and Vincent van Oostrom
Proof Orders for Decreasing Diagrams
In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013),
Leibniz International Proceedings in Informatics 21, pp. 174–189, 2013.
doi: 10.4230/LIPIcs.RTA.2013.174
-
Bertram Felgenhauer
Deciding Confluence of Ground Term Rewrite Systems in Cubic Time
In Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012),
Leibniz International Proceedings in Informatics 15, pp. 165–175, 2012.
doi: 10.4230/LIPIcs.RTA.2012.165
-
Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp
Layer Systems for Proving Confluence
In Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011),
Leibniz International Proceedings in Informatics 13, pp. 288–299, 2011.
doi: 10.4230/LIPIcs.FSTTCS.2011.288
-
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
CSI — A Confluence Tool
In Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011),,
Lecture Notes in Artificial Intelligence 6803, pp. 499–505, 2011.
© Springer
doi: 10.1007/978-3-642-22438-6_38
-
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Labelings for Decreasing Diagrams
In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011),
Leibniz International Proceedings in Informatics 10, pp. 377–392, 2011.
doi: 10.4230/LIPIcs.RTA.2011.377
Thesis
Others
-
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska Rapp
Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL
Presented by T. V. H. Prathamesh at the 7th International Workshop on Confluence (IWC 2018)
-
Bertram Felgenhauer and Jakob Grue Simonsen (editors)
Proceedings of the 7th International Workshop on Confluence (IWC 2018)
-
Bertram Felgenhauer
Minsky Machines
Formal proof development, Archive of Formal Proofs, 2018
-
Bertram Felgenhauer
Beyond DRAT: Challenges in Certifying UNSAT
Presented at the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017)
-
Bertram Felgenhauer and Franziska Rapp
Aspects of Layer Systems in IsaFoR
Presented at the 6th International Workshop on Confluence (IWC 2017)
-
Beniamino Accatolli and Bertram Felgenhauer (editors)
Proceedings of the 6th International Workshop on Confluence (IWC 2017)
-
Bertram Felgenhauer
Efficiently Deciding Uniqueness of Normal Forms and Unique Normalization for Ground TRSs
Presented at the 5th International Workshop on Confluence (IWC 2016)
-
Bertram Felgenhauer
Decreasing Diagrams II
Formal proof development, Archive of Formal Proofs, 2015
-
Bertram Felgenhauer
Point-Decreasing Diagrams Revisited
Presented at the 4th International Workshop on Confluence (IWC 2015)
-
Bertram Felgenhauer
Point-Step-Decreasing Diagrams
Presented at the 4th International Workshop on Confluence (IWC 2015)
-
Bertram Felgenhauer
Labeling Multi-Steps for Confluence of Left-Linear Term Rewrite Systems
Presented at the 4th International Workshop on Confluence (IWC 2015)
-
Martin Avanzini and Bertram Felgenhauer
Type Introduction for Runtime Complexity Analysis
For the 14th International Workshop on Termination (WST 2014)
-
Bertram Felgenhauer
Rule Labeling for Confluence of Left-Linear Term Rewrite Systems
Presented at the 2nd International Workshop on Confluence (IWC 2013)
-
Bertram Felgenhauer, Martin Avanzini, and Christian Sternagel
A Haskell Library for Term Rewriting
Presented at the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013)
-
Bertram Felgenhauer
A Proof Order for Decreasing Diagrams
Presented at the 1st International Workshop on Confluence (IWC 2012)
-
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
CoCo 2012 Participant: CSI
Presented at the 1st International Workshop on Confluence (IWC 2012)
-
Bertram Felgenhauer
Binomial Interpretations
Presented at the 12th International Workshop on Termination (WST 2012)