Improving Dependency Pairs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (LPAR, 2003)

Size-Change Termination for Term Rewriting. - René Thiemann; Jürgen Giesl (RTA, 2003)

Improved Modular Termination Proofs Using Dependency Pairs. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (IJCAR, 2004)

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (LPAR, 2004)

Automated Termination Proofs with AProVE. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (RTA, 2004)

Proving and Disproving Termination in the Dependency Pair Framework. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (Deduction and Applications, 2005)

Proving and Disproving Termination of Higher-Order Functions. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp (FroCoS, 2005)

The size-change principle and dependency pairs for termination of term rewriting. - René Thiemann; Jürgen Giesl (Appl. Algebra Eng. Commun. Comput., 2005)

Automatic Termination Proofs in the Dependency Pair Framework. - Jürgen Giesl; Peter Schneider-Kamp; René Thiemann (IJCAR, 2006)

Automated Termination Analysis for Logic Programs by Term Rewriting. - Peter Schneider-Kamp; Jürgen Giesl; Alexander Serebrenik; René Thiemann (LOPSTR, 2006)

SAT Solving for Argument Filterings. - Michael Codish; Peter Schneider-Kamp; Vitaly Lagoon; René Thiemann; Jürgen Giesl (LPAR, 2006)

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. - Jürgen Giesl; Stephan Swiderski; Peter Schneider-Kamp; René Thiemann (RTA, 2006)

Mechanizing and Improving Dependency Pairs. - Jürgen Giesl; René Thiemann; Peter Schneider-Kamp; Stephan Falke 001 (J. Autom. Reason., 2006)

Proving Termination by Bounded Increase. - Jürgen Giesl; René Thiemann; Stephan Swiderski; Peter Schneider-Kamp (CADE, 2007)

Termination of Programs using Term Rewriting and SAT Solving. - Jürgen Giesl; Peter Schneider-Kamp; René Thiemann; Stephan Swiderski; Manh Thang Nguyen; Danny De Schreye; Alexander Serebrenik (Deduction and Decision Procedures, 2007)

Implementing RPO and POLO using SAT. - Peter Schneider-Kamp; Carsten Fuhs; René Thiemann; Jürgen Giesl; Elena Annov; Michael Codish; Aart Middeldorp; Harald Zankl (Deduction and Decision Procedures, 2007)

Decision Procedures for Loop Detection. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (Deduction and Decision Procedures, 2007)

Proving Termination Using Recursive Path Orders and SAT Solving. - Peter Schneider-Kamp; René Thiemann; Elena Annov; Michael Codish; Jürgen Giesl (FroCoS, 2007)

SAT Solving for Termination Analysis with Polynomial Interpretations. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (SAT, 2007)

Innermost Termination of Rewrite Systems by Labeling. - René Thiemann; Aart Middeldorp (WRS@RDP, 2007)

The DP framework for proving termination of term rewriting. - René Thiemann (2007)

Improving Context-Sensitive Dependency Pairs. - Beatriz Alarcón; Fabian Emmes; Carsten Fuhs; Jürgen Giesl; Raúl Gutiérrez; Salvador Lucas; Peter Schneider-Kamp; René Thiemann (LPAR, 2008)

Maximal Termination. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (RTA, 2008)

Deciding Innermost Loops. - René Thiemann; Jürgen Giesl; Peter Schneider-Kamp (RTA, 2008)

Adding constants to string rewriting. - René Thiemann; Hans Zantema; Jürgen Giesl; Peter Schneider-Kamp (Appl. Algebra Eng. Commun. Comput., 2008)

Is our self based on reward? Self-relatedness recruits neural activity in the reward system. - Moritz de Greck; Michael Rotte; Rabea Paus; Diana Moritz; René Thiemann; U. Proesch; U. Bruer; S. Moerth; Claus Tempelmann; Bernhard Bogerts; Georg Northoff (NeuroImage, 2008)

Loops under Strategies. - René Thiemann; Christian Sternagel (RTA, 2009)

From Outermost Termination to Innermost Termination. - René Thiemann (SOFSEM, 2009)

Certification of Termination Proofs Using CeTA. - René Thiemann; Christian Sternagel (TPHOLs, 2009)

Automated termination proofs for logic programs by term rewriting. - Peter Schneider-Kamp; Jürgen Giesl; Alexander Serebrenik; René Thiemann (ACM Trans. Comput. Log., 2009)

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. - Christian Sternagel; René Thiemann (CSL, 2010)

Certified Subterm Criterion and Certified Usable Rules. - Christian Sternagel; René Thiemann (RTA, 2010)

Abstract Rewriting. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Executable Matrix Operations on Matrices of Arbitrary Dimensions. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Executable Multivariate Polynomials. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2010)

Loops under Strategies ... Continued - René Thiemann; Christian Sternagel; Jürgen Giesl; Peter Schneider-Kamp (IWS, 2010)

Automated termination analysis for logic programs with cut. - Peter Schneider-Kamp; Jürgen Giesl; Thomas Ströder; Alexander Serebrenik; René Thiemann (Theory Pract. Log. Program., 2010)

Generalized and Formalized Uncurrying. - Christian Sternagel; René Thiemann (FroCoS, 2011)

Termination of Isabelle Functions via Termination of Rewriting. - Alexander Krauss 001; Christian Sternagel; René Thiemann; Carsten Fuhs; Jürgen Giesl (ITP, 2011)

Modular and Certified Semantic Labeling and Unlabeling. - Christian Sternagel; René Thiemann (RTA, 2011)

Executable Transitive Closures of Finite Relations. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2011)

Automated termination proofs for haskell by term rewriting. - Jürgen Giesl; Matthias Raffelsieper; Peter Schneider-Kamp; Stephan Swiderski; René Thiemann (ACM Trans. Program. Lang. Syst., 2011)

Certification of Nontermination Proofs. - Christian Sternagel; René Thiemann (ITP, 2012)

On the Formalization of Termination Techniques based on Multiset Orderings. - René Thiemann; Guillaume Allais; Julian Nagele (RTA, 2012)

Executable Transitive Closures. - René Thiemann (Arch. Formal Proofs, 2012)

Generating linear orders for datatypes. - René Thiemann (Arch. Formal Proofs, 2012)

CeTA - A Tool for Certified Termination Analysis - Christian Sternagel; René Thiemann; Sarah Winkler; Harald Zankl (CoRR, 2012)

Certification extends Termination Techniques - Christian Sternagel; René Thiemann (CoRR, 2012)

A Relative Dependency Pair Framework - Christian Sternagel; René Thiemann (CoRR, 2012)

Recording Completion for Finding and Certifying Proofs in Equational Logic - Thomas Sternagel; René Thiemann; Harald Zankl; Christian Sternagel (CoRR, 2012)

Towards the Certification of Complexity Proofs - René Thiemann (CoRR, 2012)

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. - Michael Codish; Jürgen Giesl; Peter Schneider-Kamp; René Thiemann (J. Autom. Reason., 2012)

Formalizing Bounded Increase. - René Thiemann (ITP, 2013)

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. - Christian Sternagel; René Thiemann (RTA, 2013)

Computing Square Roots using the Babylonian Method. - René Thiemann (Arch. Formal Proofs, 2013)

Proving Termination of Programs Automatically with AProVE. - Jürgen Giesl; Marc Brockschmidt; Fabian Emmes; Florian Frohn; Carsten Fuhs; Carsten Otto; Martin Plücker; Peter Schneider-Kamp; Thomas Ströder; Stephanie Swiderski; René Thiemann (IJCAR, 2014)

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

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. - Christian Sternagel; René Thiemann (RTA-TLCA, 2014)

Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. - Julian Nagele; René Thiemann; Sarah Winkler (VSTTE, 2014)

Haskell's Show-Class in Isabelle/HOL. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

XML. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

Certification Monads. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2014)

Implementing field extensions of the form Q[sqrt(b)]. - René Thiemann (Arch. Formal Proofs, 2014)

Mutually Recursive Partial Functions. - René Thiemann (Arch. Formal Proofs, 2014)

Lifting Definition Option. - René Thiemann (Arch. Formal Proofs, 2014)

The Certification Problem Format. - Christian Sternagel; René Thiemann (UITP, 2014)

A Framework for Developing Stand-Alone Certifiers. - Christian Sternagel; René Thiemann (LSFA, 2014)

Termination Competition (termCOMP 2015). - Jürgen Giesl; Frédéric Mesnard; Albert Rubio; René Thiemann; Johannes Waldmann (CADE, 2015)

Formalizing Soundness and Completeness of Unravelings. - Sarah Winkler; René Thiemann (FroCos, 2015)

Deriving Comparators and Show Functions in Isabelle/HOL. - Christian Sternagel; René Thiemann (ITP, 2015)

Certification of Complexity Proofs using CeTA. - Martin Avanzini; Christian Sternagel; René Thiemann (RTA, 2015)

Deriving class instances for datatypes. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2015)

Algebraic Numbers in Isabelle/HOL. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2015)

Matrices, Jordan Normal Forms, and Spectral Radius Theory. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2015)

Certification of Confluence Proofs using CeTA. - Julian Nagele; René Thiemann (CoRR, 2015)

Preface. - Mario R. F. Benevides; René Thiemann (LSFA, 2015)

Formalizing jordan normal forms in Isabelle/HOL. - René Thiemann; Akihisa Yamada 002 (CPP, 2016)

AC Dependency Pairs Revisited. - Akihisa Yamada 002; Christian Sternagel; René Thiemann; Keiichirou Kusakari (CSL, 2016)

The Factorization Algorithm of Berlekamp and Zassenhaus. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Perron-Frobenius Theorem for Spectral Radius Analysis. - Jose Divasón; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Polynomial Factorization. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Polynomial Interpolation. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2016)

Certifying Safety and Termination Proofs for Integer Transition Systems. - Marc Brockschmidt; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (CADE, 2017)

A formalization of the Berlekamp-Zassenhaus factorization algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (CPP, 2017)

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

Subresultants. - Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2017)

Stochastic Matrices and the Perron-Frobenius Theorem. - René Thiemann (Arch. Formal Proofs, 2017)

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

Analyzing Program Termination and Complexity Automatically with AProVE. - Jürgen Giesl; Cornelius Aschermann; Marc Brockschmidt; Fabian Emmes; Florian Frohn; Carsten Fuhs; Jera Hensel; Carsten Otto; Martin Plücker; Peter Schneider-Kamp; Thomas Ströder; Stephanie Swiderski; et al. (J. Autom. Reason., 2017)

Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). - Jose Divasón; Sebastiaan J. C. Joosten; Ondrej Kuncar; René Thiemann; Akihisa Yamada 002 (CPP, 2018)

A Formalization of the LLL Basis Reduction Algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (ITP, 2018)

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (LPAR, 2018)

Extending a Verified Simplex Algorithm. - René Thiemann (LPAR (Workshop and Short Papers), 2018)

A verified LLL algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2018)

A verified factorization algorithm for integer polynomials with polynomial complexity. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2018)

An Incremental Simplex Algorithm with Unsatisfiable Core Generation. - Filip Maric; Mirko Spasic; René Thiemann (Arch. Formal Proofs, 2018)

First-Order Terms. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2018)

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (FroCos, 2019)

Farkas' Lemma and Motzkin's Transposition Theorem. - Ralph Bottesch; Max W. Haslbeck; René Thiemann (Arch. Formal Proofs, 2019)

Linear Inequalities. - Ralph Bottesch; Alban Reynaud; René Thiemann (Arch. Formal Proofs, 2019)

Logical and Semantic Frameworks with Applications. - Vivek Nigam; René Thiemann (Theor. Comput. Sci., 2019)

Certifying the Weighted Path Order (Invited Talk). - René Thiemann; Jonas Schöpf; Christian Sternagel; Akihisa Yamada 002 (FSCD, 2020)

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. - Ralph Bottesch; Max W. Haslbeck; Alban Reynaud; René Thiemann (NFM, 2020)

A Formalization of Knuth-Bendix Orders. - Christian Sternagel; René Thiemann (Arch. Formal Proofs, 2020)

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. - Jose Divasón; Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (J. Autom. Reason., 2020)

A Verified Implementation of Algebraic Numbers in Isabelle/HOL. - Sebastiaan J. C. Joosten; René Thiemann; Akihisa Yamada 002 (J. Autom. Reason., 2020)

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. - René Thiemann; Ralph Bottesch; Jose Divasón; Max W. Haslbeck; Sebastiaan J. C. Joosten; Akihisa Yamada 002 (J. Autom. Reason., 2020)

An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. - Max W. Haslbeck; René Thiemann (CPP, 2021)

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. - Ralph Bottesch; Jose Divasón; René Thiemann (Arch. Formal Proofs, 2021)

Factorization of Polynomials with Algebraic Coefficients. - Manuel Eberl; René Thiemann (Arch. Formal Proofs, 2021)

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

A Formalization of Weighted Path Orders and Recursive Path Orders. - Christian Sternagel; René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2021)

The Sunflower Lemma of Erdős and Rado. - René Thiemann (Arch. Formal Proofs, 2021)

Solving Cubic and Quartic Equations. - René Thiemann (Arch. Formal Proofs, 2021)

A Perron-Frobenius theorem for deciding matrix growth. - René Thiemann (J. Log. Algebraic Methods Program., 2021)

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines. - Christian Dalvit; René Thiemann (Arch. Formal Proofs, 2022)

Duality of Linear Programming. - René Thiemann (Arch. Formal Proofs, 2022)

Clique is not solvable by monotone circuits of polynomial size. - René Thiemann (Arch. Formal Proofs, 2022)

The Generalized Multiset Ordering is NP-Complete. - René Thiemann; Lukas Schmidinger (Arch. Formal Proofs, 2022)

A Formalization of the Smith Normal Form in Higher-Order Logic. - Jose Divasón; René Thiemann (J. Autom. Reason., 2022)

Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic. - Jose Divasón; René Thiemann (J. Autom. Reason., 2022)

A Verified Efficient Implementation of the Weighted Path Order. - René Thiemann; Elias Wenninger (Arch. Formal Proofs, 2023)

Linear Termination over N is Undecidable. - Fabian Mitterwallner; Aart Middeldorp; René Thiemann (CoRR, 2023)

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. - Nao Hirokawa; Dohan Kim 001; Kiraku Shintani; René Thiemann (CPP, 2024)

A Verified Algorithm for Deciding Pattern Completeness. - René Thiemann; Akihisa Yamada 002 (FSCD, 2024)

Linear Termination is Undecidable. - Fabian Mitterwallner; Aart Middeldorp; René Thiemann (LICS, 2024)

A Preprocessor for Linear Diophantine Equalities and Inequalities. - René Thiemann (Arch. Formal Proofs, 2024)

Undecidability Results on Orienting Single Rewrite Rules. - René Thiemann; Fabian Mitterwallner; Aart Middeldorp (Arch. Formal Proofs, 2024)

Verifying a Decision Procedure for Pattern Completeness. - René Thiemann; Akihisa Yamada 002 (Arch. Formal Proofs, 2024)

Sorted Terms. - Akihisa Yamada 002; René Thiemann (Arch. Formal Proofs, 2024)

An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. - Dohan Kim 001; Teppei Saito; René Thiemann; Akihisa Yamada 002 (CPP, 2025)

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)