René Thiemann

Orcid: 0000-0002-0323-8829

According to our database1, René Thiemann authored at least 124 papers between 2003 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2024
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs.
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023
Linear Termination over N is Undecidable.
CoRR, 2023

A Verified Efficient Implementation of the Weighted Path Order.
Arch. Formal Proofs, 2023

2022
Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic.
J. Autom. Reason., 2022

A Formalization of the Smith Normal Form in Higher-Order Logic.
J. Autom. Reason., 2022

The Generalized Multiset Ordering is NP-Complete.
Arch. Formal Proofs, 2022

Clique is not solvable by monotone circuits of polynomial size.
Arch. Formal Proofs, 2022

Duality of Linear Programming.
Arch. Formal Proofs, 2022

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines.
Arch. Formal Proofs, 2022

2021
A Perron-Frobenius theorem for deciding matrix growth.
J. Log. Algebraic Methods Program., 2021

Solving Cubic and Quartic Equations.
Arch. Formal Proofs, 2021

The Sunflower Lemma of Erdős and Rado.
Arch. Formal Proofs, 2021

A Formalization of Weighted Path Orders and Recursive Path Orders.
Arch. Formal Proofs, 2021

Regular Tree Relations.
Arch. Formal Proofs, 2021

Factorization of Polynomials with Algebraic Coefficients.
Arch. Formal Proofs, 2021

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation.
Arch. Formal Proofs, 2021

An Isabelle/HOL formalization of AProVE's termination method for LLVM IR.
Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.
J. Autom. Reason., 2020

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.
J. Autom. Reason., 2020

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.
J. Autom. Reason., 2020

A Formalization of Knuth-Bendix Orders.
Arch. Formal Proofs, 2020

Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL.
Proceedings of the NASA Formal Methods - 12th International Symposium, 2020

Certifying the Weighted Path Order (Invited Talk).
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019
Logical and Semantic Frameworks with Applications.
Theor. Comput. Sci., 2019

Linear Inequalities.
Arch. Formal Proofs, 2019

Farkas' Lemma and Motzkin's Transposition Theorem.
Arch. Formal Proofs, 2019

Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018
First-Order Terms.
Arch. Formal Proofs, 2018

An Incremental Simplex Algorithm with Unsatisfiable Core Generation.
Arch. Formal Proofs, 2018

A verified factorization algorithm for integer polynomials with polynomial complexity.
Arch. Formal Proofs, 2018

A verified LLL algorithm.
Arch. Formal Proofs, 2018

Extending a Verified Simplex Algorithm.
Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

A Formalization of the LLL Basis Reduction Algorithm.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper).
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Analyzing Program Termination and Complexity Automatically with AProVE.
J. Autom. Reason., 2017

Reachability, confluence, and termination analysis with state-compatible automata.
Inf. Comput., 2017

Stochastic Matrices and the Perron-Frobenius Theorem.
Arch. Formal Proofs, 2017

Subresultants.
Arch. Formal Proofs, 2017

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

A formalization of the Berlekamp-Zassenhaus factorization algorithm.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Certifying Safety and Termination Proofs for Integer Transition Systems.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Polynomial Interpolation.
Arch. Formal Proofs, 2016

Polynomial Factorization.
Arch. Formal Proofs, 2016

Perron-Frobenius Theorem for Spectral Radius Analysis.
Arch. Formal Proofs, 2016

The Factorization Algorithm of Berlekamp and Zassenhaus.
Arch. Formal Proofs, 2016

AC Dependency Pairs Revisited.
Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Formalizing jordan normal forms in Isabelle/HOL.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015
Preface.
Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Certification of Confluence Proofs using CeTA.
CoRR, 2015

Matrices, Jordan Normal Forms, and Spectral Radius Theory.
Arch. Formal Proofs, 2015

Algebraic Numbers in Isabelle/HOL.
Arch. Formal Proofs, 2015

Deriving class instances for datatypes.
Arch. Formal Proofs, 2015

Certification of Complexity Proofs using CeTA.
Proceedings of the 26th International Conference on Rewriting Techniques and Applications, 2015

Deriving Comparators and Show Functions in Isabelle/HOL.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Formalizing Soundness and Completeness of Unravelings.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Termination Competition (termCOMP 2015).
Proceedings of the Automated Deduction - CADE-25, 2015

2014
A Framework for Developing Stand-Alone Certifiers.
Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

The Certification Problem Format.
Proceedings of the Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, 2014

Lifting Definition Option.
Arch. Formal Proofs, 2014

Mutually Recursive Partial Functions.
Arch. Formal Proofs, 2014

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

Certification Monads.
Arch. Formal Proofs, 2014

Arch. Formal Proofs, 2014

Haskell's Show-Class in Isabelle/HOL.
Arch. Formal Proofs, 2014

Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Reachability Analysis with State-Compatible Automata.
Proceedings of the Language and Automata Theory and Applications, 2014

Proving Termination of Programs Automatically with AProVE.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
Computing Square Roots using the Babylonian Method.
Arch. Formal Proofs, 2013

Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion.
Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Formalizing Bounded Increase.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs.
J. Autom. Reason., 2012

Towards the Certification of Complexity Proofs
CoRR, 2012

Recording Completion for Finding and Certifying Proofs in Equational Logic
CoRR, 2012

A Relative Dependency Pair Framework
CoRR, 2012

Certification extends Termination Techniques
CoRR, 2012

CeTA - A Tool for Certified Termination Analysis
CoRR, 2012

Generating linear orders for datatypes.
Arch. Formal Proofs, 2012

Executable Transitive Closures.
Arch. Formal Proofs, 2012

On the Formalization of Termination Techniques based on Multiset Orderings.
Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012

Certification of Nontermination Proofs.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011
Automated termination proofs for haskell by term rewriting.
ACM Trans. Program. Lang. Syst., 2011

Executable Transitive Closures of Finite Relations.
Arch. Formal Proofs, 2011

Modular and Certified Semantic Labeling and Unlabeling.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Termination of Isabelle Functions via Termination of Rewriting.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Generalized and Formalized Uncurrying.
Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010
Automated termination analysis for logic programs with cut.
Theory Pract. Log. Program., 2010

Loops under Strategies ... Continued
Proceedings of the Proceedings International Workshop on Strategies in Rewriting, 2010

Executable Multivariate Polynomials.
Arch. Formal Proofs, 2010

Executable Matrix Operations on Matrices of Arbitrary Dimensions.
Arch. Formal Proofs, 2010

Abstract Rewriting.
Arch. Formal Proofs, 2010

Certified Subterm Criterion and Certified Usable Rules.
Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009
Automated termination proofs for logic programs by term rewriting.
ACM Trans. Comput. Log., 2009

Certification of Termination Proofs Using CeTA.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

From Outermost Termination to Innermost Termination.
Proceedings of the SOFSEM 2009: Theory and Practice of Computer Science, 2009

Loops under Strategies.
Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

2008
Is our self based on reward? Self-relatedness recruits neural activity in the reward system.
NeuroImage, 2008

Adding constants to string rewriting.
Appl. Algebra Eng. Commun. Comput., 2008

Deciding Innermost Loops.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Maximal Termination.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Improving Context-Sensitive Dependency Pairs.
Proceedings of the Logic for Programming, 2008

2007
The DP framework for proving termination of term rewriting.
PhD thesis, 2007

Innermost Termination of Rewrite Systems by Labeling.
Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

SAT Solving for Termination Analysis with Polynomial Interpretations.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Proving Termination Using Recursive Path Orders and SAT Solving.
Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

Decision Procedures for Loop Detection.
Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Implementing RPO and POLO using SAT.
Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Termination of Programs using Term Rewriting and SAT Solving.
Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

Proving Termination by Bounded Increase.
Proceedings of the Automated Deduction, 2007

2006
Mechanizing and Improving Dependency Pairs.
J. Autom. Reason., 2006

Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

SAT Solving for Argument Filterings.
Proceedings of the Logic for Programming, 2006

Automated Termination Analysis for Logic Programs by Term Rewriting.
Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

Automatic Termination Proofs in the Dependency Pair Framework.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
The size-change principle and dependency pairs for termination of term rewriting.
Appl. Algebra Eng. Commun. Comput., 2005

Proving and Disproving Termination of Higher-Order Functions.
Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

Proving and Disproving Termination in the Dependency Pair Framework.
Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

2004
Automated Termination Proofs with AProVE.
Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs.
Proceedings of the Logic for Programming, 2004

Improved Modular Termination Proofs Using Dependency Pairs.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Size-Change Termination for Term Rewriting.
Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Improving Dependency Pairs.
Proceedings of the Logic for Programming, 2003


  Loading...