René Thiemann

ORCID

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 65

Top Venues

RWTH Aachen University, Germany (PHD)

Education History

RWTH Aachen University, Germany

PHD

Publications

René Thiemann, Akihisa Yamada
A Verified Algorithm for Deciding Pattern Completeness. FSCD (2024)
Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. CPP (2024)
René Thiemann, Akihisa Yamada
Verifying a Decision Procedure for Pattern Completeness. Arch. Formal Proofs 2024 (2024)
René Thiemann
A Preprocessor for Linear Diophantine Equalities and Inequalities. Arch. Formal Proofs 2024 (2024)
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Linear Termination is Undecidable. LICS (2024)
Akihisa Yamada, René Thiemann
Sorted Terms. Arch. Formal Proofs 2024 (2024)
René Thiemann, Fabian Mitterwallner, Aart Middeldorp
Undecidability Results on Orienting Single Rewrite Rules. Arch. Formal Proofs 2024 (2024)
René Thiemann, Elias Wenninger
A Verified Efficient Implementation of the Weighted Path Order. CoRR (2023)
René Thiemann, Elias Wenninger
A Verified Efficient Implementation of the Weighted Path Order. Arch. Formal Proofs 2023 (2023)
Fabian Mitterwallner, Aart Middeldorp, René Thiemann
Linear Termination over N is Undecidable. CoRR (2023)
René Thiemann
Clique is not solvable by monotone circuits of polynomial size. Arch. Formal Proofs 2022 (2022)
René Thiemann
Duality of Linear Programming. Arch. Formal Proofs 2022 (2022)
Jose Divasón, René Thiemann
A Formalization of the Smith Normal Form in Higher-Order Logic. J. Autom. Reason. 66 (4) (2022)
René Thiemann, Lukas Schmidinger
The Generalized Multiset Ordering is NP-Complete. Arch. Formal Proofs 2022 (2022)
Jose Divasón, René Thiemann
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic. J. Autom. Reason. 66 (4) (2022)
Christian Dalvit, René Thiemann
A Verified Translation of Multitape Turing Machines into Singletape Turing Machines. Arch. Formal Proofs 2022 (2022)
René Thiemann
The Sunflower Lemma of Erdős and Rado. Arch. Formal Proofs 2021 (2021)
Max W. Haslbeck, René Thiemann
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. CPP (2021)
Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
Regular Tree Relations. Arch. Formal Proofs 2021 (2021)
Manuel Eberl, René Thiemann
Factorization of Polynomials with Algebraic Coefficients. Arch. Formal Proofs 2021 (2021)
Ralph Bottesch, Jose Divasón, René Thiemann
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation. Arch. Formal Proofs 2021 (2021)
René Thiemann
A Perron-Frobenius theorem for deciding matrix growth. J. Log. Algebraic Methods Program. 123 (2021)
Christian Sternagel, René Thiemann, Akihisa Yamada
A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs 2021 (2021)
René Thiemann
Solving Cubic and Quartic Equations. Arch. Formal Proofs 2021 (2021)
Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. NFM (2020)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reason. 64 (4) (2020)
René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. J. Autom. Reason. 64 (5) (2020)
René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
Certifying the Weighted Path Order (Invited Talk). FSCD (2020)
Christian Sternagel, René Thiemann
A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs 2020 (2020)
Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. J. Autom. Reason. 64 (3) (2020)
Ralph Bottesch, Alban Reynaud, René Thiemann
Linear Inequalities. Arch. Formal Proofs 2019 (2019)
Ralph Bottesch, Max W. Haslbeck, René Thiemann
Farkas' Lemma and Motzkin's Transposition Theorem. Arch. Formal Proofs 2019 (2019)
Vivek Nigam, René Thiemann
Logical and Semantic Frameworks with Applications. Theor. Comput. Sci. 781 (2019)
Ralph Bottesch, Max W. Haslbeck, René Thiemann
Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL. FroCos (2019)
Ralph Bottesch, Max W. Haslbeck, René Thiemann
A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. LPAR (2018)
René Thiemann
Extending a Verified Simplex Algorithm. LPAR (Workshop and Short Papers) (2018)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A verified LLL algorithm. Arch. Formal Proofs 2018 (2018)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A verified factorization algorithm for integer polynomials with polynomial complexity. Arch. Formal Proofs 2018 (2018)
Filip Maric, Mirko Spasic, René Thiemann
An Incremental Simplex Algorithm with Unsatisfiable Core Generation. Arch. Formal Proofs 2018 (2018)
Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP (2018)
Christian Sternagel, René Thiemann
First-Order Terms. Arch. Formal Proofs 2018 (2018)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A Formalization of the LLL Basis Reduction Algorithm. ITP (2018)
Bertram Felgenhauer, René Thiemann
Reachability, confluence, and termination analysis with state-compatible automata. Inf. Comput. 253 (2017)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP (2017)
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
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS (2017)
René Thiemann
Stochastic Matrices and the Perron-Frobenius Theorem. Arch. Formal Proofs 2017 (2017)
Marc Brockschmidt, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Certifying Safety and Termination Proofs for Integer Transition Systems. CADE (2017)
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
Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58 (1) (2017)
Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Subresultants. Arch. Formal Proofs 2017 (2017)
Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada
Perron-Frobenius Theorem for Spectral Radius Analysis. Arch. Formal Proofs 2016 (2016)
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
The Factorization Algorithm of Berlekamp and Zassenhaus. Arch. Formal Proofs 2016 (2016)
Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari
AC Dependency Pairs Revisited. CSL (2016)
René Thiemann, Akihisa Yamada
Polynomial Factorization. Arch. Formal Proofs 2016 (2016)
René Thiemann, Akihisa Yamada
Polynomial Interpolation. Arch. Formal Proofs 2016 (2016)
René Thiemann, Akihisa Yamada
Formalizing jordan normal forms in Isabelle/HOL. CPP (2016)
René Thiemann, Akihisa Yamada
Algebraic Numbers in Isabelle/HOL. ITP (2016)
Christian Sternagel, René Thiemann
Deriving class instances for datatypes. Arch. Formal Proofs 2015 (2015)
Christian Sternagel, René Thiemann
Deriving Comparators and Show Functions in Isabelle/HOL. ITP (2015)
Mario R. F. Benevides, René Thiemann
Preface. LSFA (2015)
René Thiemann, Akihisa Yamada
Algebraic Numbers in Isabelle/HOL. Arch. Formal Proofs 2015 (2015)
Martin Avanzini, Christian Sternagel, René Thiemann
Certification of Complexity Proofs using CeTA. RTA (2015)
Julian Nagele, René Thiemann
Certification of Confluence Proofs using CeTA. CoRR (2015)
René Thiemann, Akihisa Yamada
Matrices, Jordan Normal Forms, and Spectral Radius Theory. Arch. Formal Proofs 2015 (2015)
Sarah Winkler, René Thiemann
Formalizing Soundness and Completeness of Unravelings. FroCos (2015)
Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann
Termination Competition (termCOMP 2015). CADE (2015)
René Thiemann
Mutually Recursive Partial Functions. Arch. Formal Proofs 2014 (2014)
Julian Nagele, René Thiemann, Sarah Winkler
Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. VSTTE (2014)
Christian Sternagel, René Thiemann
Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs 2014 (2014)
Bertram Felgenhauer, René Thiemann
Reachability Analysis with State-Compatible Automata. LATA (2014)
René Thiemann
Implementing field extensions of the form Q[sqrt(b)]. Arch. Formal Proofs 2014 (2014)
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
Proving Termination of Programs Automatically with AProVE. IJCAR (2014)
Christian Sternagel, René Thiemann
A Framework for Developing Stand-Alone Certifiers. LSFA (2014)
Christian Sternagel, René Thiemann
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA (2014)
René Thiemann
Lifting Definition Option. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
Certification Monads. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
XML. Arch. Formal Proofs 2014 (2014)
Christian Sternagel, René Thiemann
The Certification Problem Format. UITP (2014)
René Thiemann
Formalizing Bounded Increase. ITP (2013)
Christian Sternagel, René Thiemann
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA (2013)
René Thiemann
Computing Square Roots using the Babylonian Method. Arch. Formal Proofs 2013 (2013)
René Thiemann, Guillaume Allais, Julian Nagele
On the Formalization of Termination Techniques based on Multiset Orderings. RTA (2012)
René Thiemann
Towards the Certification of Complexity Proofs CoRR (2012)
Christian Sternagel, René Thiemann
Certification of Nontermination Proofs. ITP (2012)
Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl
CeTA - A Tool for Certified Termination Analysis CoRR (2012)
Christian Sternagel, René Thiemann
Certification extends Termination Techniques CoRR (2012)
René Thiemann
Executable Transitive Closures. Arch. Formal Proofs 2012 (2012)
Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann
SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. J. Autom. Reason. 49 (1) (2012)
Christian Sternagel, René Thiemann
A Relative Dependency Pair Framework CoRR (2012)
Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel
Recording Completion for Finding and Certifying Proofs in Equational Logic CoRR (2012)
René Thiemann
Generating linear orders for datatypes. Arch. Formal Proofs 2012 (2012)
Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, René Thiemann
Automated termination proofs for haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33 (2) (2011)
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
Termination of Isabelle Functions via Termination of Rewriting. ITP (2011)
Christian Sternagel, René Thiemann
Generalized and Formalized Uncurrying. FroCoS (2011)
Christian Sternagel, René Thiemann
Modular and Certified Semantic Labeling and Unlabeling. RTA (2011)
Christian Sternagel, René Thiemann
Executable Transitive Closures of Finite Relations. Arch. Formal Proofs 2011 (2011)
Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann
Automated Termination Analysis for Logic Programs with Cut CoRR (2010)
Christian Sternagel, René Thiemann
Abstract Rewriting. Arch. Formal Proofs 2010 (2010)
Peter Schneider-Kamp, Jürgen Giesl, Thomas Ströder, Alexander Serebrenik, René Thiemann
Automated termination analysis for logic programs with cut. Theory Pract. Log. Program. 10 (4-6) (2010)
Christian Sternagel, René Thiemann
Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs 2010 (2010)
Christian Sternagel, René Thiemann
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL (2010)

René Thiemann.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

René Thiemann