René Thiemann

140 papers A* 1A 7B 23C 2Journal 73Unranked 31

Year	Rank	Type	Title / Venue / Authors
2026	—	`ed.`	Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings FroCoS René Thiemann, Christoph Weidenbach
2025	B	`conf`	An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. CPP Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada
2025	J	`jnl`	First-Order Rewriting. Arch. Formal Proofs René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada
2024	J	`jnl`	A Preprocessor for Linear Diophantine Equalities and Inequalities. Arch. Formal Proofs René Thiemann
2024	B	`conf`	A Verified Algorithm for Deciding Pattern Completeness. FSCD René Thiemann, Akihisa Yamada
2024	B	`conf`	Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. CPP Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
2024	A*	`conf`	Linear Termination is Undecidable. LICS Fabian Mitterwallner, Aart Middeldorp, René Thiemann
2024	J	`jnl`	Sorted Terms. Arch. Formal Proofs Akihisa Yamada, René Thiemann
2024	J	`jnl`	Undecidability Results on Orienting Single Rewrite Rules. Arch. Formal Proofs René Thiemann, Fabian Mitterwallner, Aart Middeldorp
2024	J	`jnl`	Verifying a Decision Procedure for Pattern Completeness. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2023	B	`ed.`	14th International Conference on Interactive Theorem Proving, ITP 2023, Białystok, Poland, July 31 - August 4, 2023 ITP Adam Naumowicz, René Thiemann
2023	J	`jnl`	A Verified Efficient Implementation of the Weighted Path Order. Arch. Formal Proofs René Thiemann, Elias Wenninger
2023	J	`jnl`	A Verified Efficient Implementation of the Weighted Path Order. CoRR René Thiemann, Elias Wenninger
2023	J	`jnl`	Linear Termination over N is Undecidable. CoRR Fabian Mitterwallner, Aart Middeldorp, René Thiemann
2022	J	`jnl`	A Formalization of the Smith Normal Form in Higher-Order Logic. J. Autom. Reason. Jose Divasón, René Thiemann
2022	J	`jnl`	A Verified Translation of Multitape Turing Machines into Singletape Turing Machines. Arch. Formal Proofs Christian Dalvit, René Thiemann
2022	J	`jnl`	Clique is not solvable by monotone circuits of polynomial size. Arch. Formal Proofs René Thiemann
2022	J	`jnl`	Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic. J. Autom. Reason. Jose Divasón, René Thiemann
2022	J	`jnl`	Duality of Linear Programming. Arch. Formal Proofs René Thiemann
2022	J	`jnl`	The Generalized Multiset Ordering is NP-Complete. Arch. Formal Proofs René Thiemann, Lukas Schmidinger
2021	J	`jnl`	A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs Christian Sternagel, René Thiemann, Akihisa Yamada
2021	J	`jnl`	A Perron-Frobenius theorem for deciding matrix growth. J. Log. Algebraic Methods Program. René Thiemann
2021	B	`conf`	An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. CPP Max W. Haslbeck, René Thiemann
2021	J	`jnl`	Factorization of Polynomials with Algebraic Coefficients. Arch. Formal Proofs Manuel Eberl, René Thiemann
2021	J	`jnl`	Regular Tree Relations. Arch. Formal Proofs Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
2021	J	`jnl`	Solving Cubic and Quartic Equations. Arch. Formal Proofs René Thiemann
2021	J	`jnl`	The Sunflower Lemma of Erdős and Rado. Arch. Formal Proofs René Thiemann
2021	J	`jnl`	Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. Arch. Formal Proofs Ralph Bottesch, Jose Divasón, René Thiemann
2020	J	`jnl`	A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs Christian Sternagel, René Thiemann
2020	J	`jnl`	A Verified Implementation of Algebraic Numbers in Isabelle/HOL. J. Autom. Reason. Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2020	J	`jnl`	A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reason. Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2020	B	`conf`	Certifying the Weighted Path Order (Invited Talk). FSCD René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
2020	J	`jnl`	Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. J. Autom. Reason. René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada
2020	—	`conf`	Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. NFM Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
2019	J	`jnl`	Farkas' Lemma and Motzkin's Transposition Theorem. Arch. Formal Proofs Ralph Bottesch, Max W. Haslbeck, René Thiemann
2019	J	`jnl`	Linear Inequalities. Arch. Formal Proofs Ralph Bottesch, Alban Reynaud, René Thiemann
2019	J	`jnl`	Logical and Semantic Frameworks with Applications. Theor. Comput. Sci. Vivek Nigam, René Thiemann
2019	—	`conf`	Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL. FroCos Ralph Bottesch, Max W. Haslbeck, René Thiemann
2018	B	`conf`	A Formalization of the LLL Basis Reduction Algorithm. ITP Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	B	`conf`	A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. LPAR Ralph Bottesch, Max W. Haslbeck, René Thiemann
2018	J	`jnl`	A verified LLL algorithm. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	J	`jnl`	A verified factorization algorithm for integer polynomials with polynomial complexity. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2018	J	`jnl`	An Incremental Simplex Algorithm with Unsatisfiable Core Generation. Arch. Formal Proofs Filip Maric, Mirko Spasic, René Thiemann
2018	B	`conf`	Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2018	—	`conf`	Extending a Verified Simplex Algorithm. LPAR (Workshop and Short Papers) René Thiemann
2018	J	`jnl`	First-Order Terms. Arch. Formal Proofs Christian Sternagel, René Thiemann
2017	B	`conf`	A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2017	J	`jnl`	Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 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, René Thiemann
2017	A	`conf`	Certifying Safety and Termination Proofs for Integer Transition Systems. CADE Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
2017	J	`jnl`	Reachability, confluence, and termination analysis with state-compatible automata. Inf. Comput. Bertram Felgenhauer, René Thiemann
2017	J	`jnl`	Stochastic Matrices and the Perron-Frobenius Theorem. Arch. Formal Proofs René Thiemann
2017	J	`jnl`	Subresultants. Arch. Formal Proofs Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2016	B	`conf`	AC Dependency Pairs Revisited. CSL Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari
2016	B	`conf`	Algebraic Numbers in Isabelle/HOL. ITP René Thiemann, Akihisa Yamada
2016	B	`conf`	Formalizing jordan normal forms in Isabelle/HOL. CPP René Thiemann, Akihisa Yamada
2016	J	`jnl`	Perron-Frobenius Theorem for Spectral Radius Analysis. Arch. Formal Proofs Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada
2016	J	`jnl`	Polynomial Factorization. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2016	J	`jnl`	Polynomial Interpolation. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2016	—	`ed.`	Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2015, Natal, Brazil, August 31 - September 1, 2015 LSFA Mario R. F. Benevides, René Thiemann
2016	J	`jnl`	The Factorization Algorithm of Berlekamp and Zassenhaus. Arch. Formal Proofs Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
2015	J	`jnl`	Algebraic Numbers in Isabelle/HOL. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2015	—	`conf`	Certification of Complexity Proofs using CeTA. RTA Martin Avanzini, Christian Sternagel, René Thiemann
2015	J	`jnl`	Certification of Confluence Proofs using CeTA. CoRR Julian Nagele, René Thiemann
2015	B	`conf`	Deriving Comparators and Show Functions in Isabelle/HOL. ITP Christian Sternagel, René Thiemann
2015	J	`jnl`	Deriving class instances for datatypes. Arch. Formal Proofs Christian Sternagel, René Thiemann
2015	—	`conf`	Formalizing Soundness and Completeness of Unravelings. FroCos Sarah Winkler, René Thiemann
2015	J	`jnl`	Matrices, Jordan Normal Forms, and Spectral Radius Theory. Arch. Formal Proofs René Thiemann, Akihisa Yamada
2015	—	`conf`	Preface. LSFA Mario R. F. Benevides, René Thiemann
2015	A	`conf`	Termination Competition (termCOMP 2015). CADE Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann
2014	—	`conf`	A Framework for Developing Stand-Alone Certifiers. LSFA Christian Sternagel, René Thiemann
2014	J	`jnl`	Certification Monads. Arch. Formal Proofs Christian Sternagel, René Thiemann
2014	—	`conf`	Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. VSTTE Julian Nagele, René Thiemann, Sarah Winkler
2014	—	`conf`	Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA Christian Sternagel, René Thiemann
2014	J	`jnl`	Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs Christian Sternagel, René Thiemann
2014	J	`jnl`	Implementing field extensions of the form Q[sqrt(b)]. Arch. Formal Proofs René Thiemann
2014	J	`jnl`	Lifting Definition Option. Arch. Formal Proofs René Thiemann
2014	J	`jnl`	Mutually Recursive Partial Functions. Arch. Formal Proofs René Thiemann
2014	A	`conf`	Proving Termination of Programs Automatically with AProVE. IJCAR 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
2014	C	`conf`	Reachability Analysis with State-Compatible Automata. LATA Bertram Felgenhauer, René Thiemann
2014	—	`conf`	The Certification Problem Format. UITP Christian Sternagel, René Thiemann
2014	J	`jnl`	XML. Arch. Formal Proofs Christian Sternagel, René Thiemann
2013	J	`jnl`	Computing Square Roots using the Babylonian Method. Arch. Formal Proofs René Thiemann
2013	B	`conf`	Formalizing Bounded Increase. ITP René Thiemann
2013	—	`conf`	Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA Christian Sternagel, René Thiemann
2012	J	`jnl`	A Relative Dependency Pair Framework CoRR Christian Sternagel, René Thiemann
2012	J	`jnl`	CeTA - A Tool for Certified Termination Analysis CoRR Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl
2012	J	`jnl`	Certification extends Termination Techniques CoRR Christian Sternagel, René Thiemann
2012	B	`conf`	Certification of Nontermination Proofs. ITP Christian Sternagel, René Thiemann
2012	J	`jnl`	Executable Transitive Closures. Arch. Formal Proofs René Thiemann
2012	J	`jnl`	Generating linear orders for datatypes. Arch. Formal Proofs René Thiemann
2012	—	`conf`	On the Formalization of Termination Techniques based on Multiset Orderings. RTA René Thiemann, Guillaume Allais, Julian Nagele
2012	J	`jnl`	Recording Completion for Finding and Certifying Proofs in Equational Logic CoRR Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel
2012	J	`jnl`	SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. J. Autom. Reason. Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann
2012	J	`jnl`	Towards the Certification of Complexity Proofs CoRR René Thiemann
2011	J	`jnl`	Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, René Thiemann
2011	J	`jnl`	Executable Transitive Closures of Finite Relations. Arch. Formal Proofs Christian Sternagel, René Thiemann
2011	—	`conf`	Generalized and Formalized Uncurrying. FroCoS Christian Sternagel, René Thiemann
2011	—	`conf`	Modular and Certified Semantic Labeling and Unlabeling. RTA Christian Sternagel, René Thiemann
2011	B	`conf`	Termination of Isabelle Functions via Termination of Rewriting. ITP Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
2010	J	`jnl`	Abstract Rewriting. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	J	`jnl`	Automated Termination Analysis for Logic Programs with Cut CoRR Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann
2010	J	`jnl`	Automated termination analysis for logic programs with cut. Theory Pract. Log. Program. Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann
2010	—	`conf`	Certified Subterm Criterion and Certified Usable Rules. RTA Christian Sternagel, René Thiemann
2010	J	`jnl`	Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	J	`jnl`	Executable Multivariate Polynomials. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	—	`conf`	Loops under Strategies ... Continued IWS René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp
2010	B	`conf`	Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL Christian Sternagel, René Thiemann
2009	J	`jnl`	Automated termination proofs for logic programs by term rewriting. ACM Trans. Comput. Log. Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, René Thiemann
2009	—	`conf`	Certification of Termination Proofs Using CeTA. TPHOLs René Thiemann, Christian Sternagel
2009	B	`conf`	From Outermost Termination to Innermost Termination. SOFSEM René Thiemann
2009	—	`conf`	Loops under Strategies. RTA René Thiemann, Christian Sternagel
2008	J	`jnl`	Adding constants to string rewriting. Appl. Algebra Eng. Commun. Comput. René Thiemann, Hans Zantema, Jürgen Giesl, Peter Schneider-Kamp
2008	J	`jnl`	Automated Termination Proofs for Logic Programs by Term Rewriting CoRR Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, René Thiemann
2008	—	`conf`	Deciding Innermost Loops. RTA René Thiemann, Jürgen Giesl, Peter Schneider-Kamp
2008	B	`conf`	Improving Context-Sensitive Dependency Pairs. LPAR Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann
2008	J	`jnl`	Is our self based on reward? Self-relatedness recruits neural activity in the reward system. NeuroImage Moritz de Greck, Michael Rotte, Rabea Paus, Diana Moritz, René Thiemann, U. Proesch, U. Bruer, S. Moerth, Claus Tempelmann, Bernhard Bogerts, Georg Northoff
2008	—	`conf`	Maximal Termination. RTA Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl
2007	—	`conf`	Decision Procedures for Loop Detection. Deduction and Decision Procedures René Thiemann, Jürgen Giesl, Peter Schneider-Kamp
2007	—	`conf`	Implementing RPO and POLO using SAT. Deduction and Decision Procedures Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, Harald Zankl
2007	—	`conf`	Innermost Termination of Rewrite Systems by Labeling. WRS@RDP René Thiemann, Aart Middeldorp
2007	—	`conf`	Proving Termination Using Recursive Path Orders and SAT Solving. FroCoS Peter Schneider-Kamp, René Thiemann, Elena Annov, Michael Codish, Jürgen Giesl
2007	A	`conf`	Proving Termination by Bounded Increase. CADE Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp
2007	A	`conf`	SAT Solving for Termination Analysis with Polynomial Interpretations. SAT Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl
2007	—	`conf`	Termination of Programs using Term Rewriting and SAT Solving. Deduction and Decision Procedures Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Danny De Schreye, Alexander Serebrenik
2007	—	`—`	The DP framework for proving termination of term rewriting. René Thiemann
2006	—	`conf`	Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. RTA Jürgen Giesl, Stephan Swiderski, Peter Schneider-Kamp, René Thiemann
2006	C	`conf`	Automated Termination Analysis for Logic Programs by Term Rewriting. LOPSTR Peter Schneider-Kamp, Jürgen Giesl, Alexander Serebrenik, René Thiemann
2006	A	`conf`	Automatic Termination Proofs in the Dependency Pair Framework. IJCAR Jürgen Giesl, Peter Schneider-Kamp, René Thiemann
2006	J	`jnl`	Mechanizing and Improving Dependency Pairs. J. Autom. Reason. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
2006	J	`jnl`	SAT Solving for Argument Filterings CoRR Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, René Thiemann, Jürgen Giesl
2006	B	`conf`	SAT Solving for Argument Filterings. LPAR Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, René Thiemann, Jürgen Giesl
2005	—	`conf`	Proving and Disproving Termination in the Dependency Pair Framework. Deduction and Applications Jürgen Giesl, René Thiemann, Peter Schneider-Kamp
2005	—	`conf`	Proving and Disproving Termination of Higher-Order Functions. FroCoS Jürgen Giesl, René Thiemann, Peter Schneider-Kamp
2005	J	`jnl`	The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput. René Thiemann, Jürgen Giesl
2004	—	`conf`	Automated Termination Proofs with AProVE. RTA Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
2004	A	`conf`	Improved Modular Termination Proofs Using Dependency Pairs. IJCAR René Thiemann, Jürgen Giesl, Peter Schneider-Kamp
2004	B	`conf`	The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. LPAR Jürgen Giesl, René Thiemann, Peter Schneider-Kamp
2003	B	`conf`	Improving Dependency Pairs. LPAR Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
2003	—	`conf`	Size-Change Termination for Term Rewriting. RTA René Thiemann, Jürgen Giesl