René Thiemann

Available identifiers

zbMath Open thiemann.reneMaRDI QIDQ515686

List of research outcomes

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

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: René Thiemann