| Publication | Date of Publication | Type |
|---|
| A formalization of the Smith normal form in higher-order logic | 2022-12-12 | Paper |
| Correction to: ``A formalization of the Smith normal form in higher-order logic | 2022-12-12 | Paper |
| A Perron-Frobenius theorem for deciding matrix growth | 2021-11-03 | Paper |
| Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL | 2020-11-02 | Paper |
| On the Formalization of Termination Techniques based on Multiset Orderings | 2020-05-27 | Paper |
| Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL | 2020-05-13 | Paper |
| A verified implementation of the Berlekamp-Zassenhaus factorization algorithm | 2020-04-07 | Paper |
| A verified implementation of algebraic numbers in Isabelle/HOL | 2020-03-03 | Paper |
| A Verified Efficient Implementation of the LLL Basis Reduction Algorithm | 2019-07-04 | Paper |
| A formalization of the LLL basis reduction algorithm | 2018-10-04 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
| Certifying safety and termination proofs for integer transition systems | 2017-09-22 | Paper |
| AC Dependency Pairs Revisited | 2017-07-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5277869 | 2017-07-12 | Paper |
| Analyzing program termination and complexity automatically with \textsf{AProVE} | 2017-07-10 | Paper |
| Reachability, confluence, and termination analysis with state-compatible automata | 2017-03-16 | Paper |
| Formalizing Soundness and Completeness of Unravelings | 2017-02-27 | Paper |
| Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion | 2017-02-01 | Paper |
| Algebraic Numbers in Isabelle/HOL | 2016-10-27 | Paper |
| A framework for developing stand-alone certifiers | 2016-08-01 | Paper |
| Termination Competition (termCOMP 2015) | 2015-12-02 | Paper |
| Automated termination proofs for logic programs by term rewriting | 2015-09-17 | Paper |
| Deriving Comparators and Show Functions in Isabelle/HOL | 2015-09-14 | Paper |
| Proving Termination of Programs Automatically with AProVE | 2014-09-26 | Paper |
| Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs | 2014-07-24 | Paper |
| Reachability Analysis with State-Compatible Automata | 2014-03-31 | Paper |
| Innermost Termination of Rewrite Systems by Labeling | 2014-01-24 | Paper |
| Formalizing Bounded Increase | 2013-08-07 | Paper |
| SAT solving for termination proofs with recursive path orders and dependency pairs | 2013-08-01 | Paper |
| Certification of Nontermination Proofs | 2012-09-20 | Paper |
| CERTIFIED SUBTERM CRITERION AND CERTIFIED USABLE RULES | 2012-04-25 | Paper |
| Modular and Certified Semantic Labeling and Unlabeling | 2012-04-24 | Paper |
| Generalized and Formalized Uncurrying | 2011-10-07 | Paper |
| Termination of Isabelle Functions via Termination of Rewriting | 2011-08-17 | Paper |
| Signature Extensions Preserve Termination | 2010-09-03 | Paper |
| Automated termination analysis for logic programs with cut | 2010-08-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3408137 | 2010-02-24 | Paper |
| Certification of Termination Proofs Using CeTA | 2009-10-20 | Paper |
| Loops under Strategies | 2009-06-30 | Paper |
| SAT Solving for Termination Analysis with Polynomial Interpretations | 2009-03-10 | Paper |
| Proving Termination by Bounded Increase | 2009-03-06 | Paper |
| From Outermost Termination to Innermost Termination | 2009-02-03 | Paper |
| Improving Context-Sensitive Dependency Pairs | 2009-01-27 | Paper |
| Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages | 2008-09-25 | Paper |
| Proving Termination Using Recursive Path Orders and SAT Solving | 2008-09-16 | Paper |
| Adding constants to string rewriting | 2008-09-10 | Paper |
| Maximal Termination | 2008-08-28 | Paper |
| Deciding Innermost Loops | 2008-08-28 | Paper |
| SAT Solving for Argument Filterings | 2008-05-27 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| Automated Termination Analysis for Logic Programs by Term Rewriting | 2007-09-10 | Paper |
| Mechanizing and improving dependency pairs | 2007-05-03 | Paper |
| Frontiers of Combining Systems | 2006-10-10 | Paper |
| The size-change principle and dependency pairs for termination of term rewriting | 2005-11-24 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4447238 | 2004-02-16 | Paper |
