×

zbMATH — the first resource for mathematics

Thiemann, René

Compute Distance To:
Author ID: thiemann.rene Recent zbMATH articles by "Thiemann, René"
Published as: Thiemann, Rene; Thiemann, René
Documents Indexed: 55 Publications since 2003, including 1 Book

Publications by Year

Citations contained in zbMATH Open

44 Publications have been cited 337 times in 154 Documents Cited by Year
Mechanizing and improving dependency pairs. Zbl 1113.68088
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
40
2006
The dependency pair framework: Combining techniques for automated termination proofs. Zbl 1108.68477
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter
37
2005
Proving and disproving termination of higher-order functions. Zbl 1171.68714
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter
27
2005
Certification of termination proofs using CeTA. Zbl 1252.68265
Thiemann, René; Sternagel, Christian
25
2009
SAT solving for termination analysis with polynomial interpretations. Zbl 1214.68352
Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald
22
2007
Automated termination analysis for Haskell: from term rewriting to programming languages. Zbl 1151.68444
Giesl, Jürgen; Swiderski, Stephan; Schneider-Kamp, Peter; Thiemann, René
19
2006
Proving termination of programs automatically with AProVE. Zbl 1409.68256
Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René
13
2014
Automated termination proofs for logic programs by term rewriting. Zbl 1351.68054
Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René
11
2009
Improved modular termination proofs using dependency pairs. Zbl 1126.68582
Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter
10
2004
Improving dependency pairs. Zbl 1273.68320
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
10
2003
The size-change principle and dependency pairs for termination of term rewriting. Zbl 1101.68640
Thiemann, René; Giesl, Jürgen
9
2005
Automated termination analysis for logic programs with cut. Zbl 1209.68098
Schneider-Kamp, Peter; Giesl, Jürgen; Ströder, Thomas; Serebrenik, Alexander; Thiemann, René
8
2010
Maximal termination. Zbl 1145.68446
Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald
8
2008
Automated termination analysis for logic programs by term rewriting. Zbl 1196.68036
Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René
8
2007
Proving termination by bounded increase. Zbl 1213.68347
Giesl, Jürgen; Thiemann, René; Swiderski, Stephan; Schneider-Kamp, Peter
7
2007
Proving termination using recursive path orders and SAT solving. Zbl 1148.68393
Schneider-Kamp, Peter; Thiemann, René; Annov, Elena; Codish, Michael; Giesl, Jürgen
7
2007
Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255
Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René
6
2017
Improving context-sensitive dependency pairs. Zbl 1182.68092
Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René
6
2008
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 06821624
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
5
2017
Algebraic numbers in Isabelle/HOL. Zbl 06644756
Thiemann, René; Yamada, Akihisa
5
2016
Termination Competition (termCOMP 2015). Zbl 06515500
Giesl, Jürgen; Mesnard, Frédéric; Rubio, Albert; Thiemann, René; Waldmann, Johannes
5
2015
SAT solving for termination proofs with recursive path orders and dependency pairs. Zbl 1276.68140
Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René
5
2012
Signature extensions preserve termination. An alternative proof via dependency pairs. Zbl 1287.03032
Sternagel, Christian; Thiemann, René
5
2010
Formalizing Knuth-Bendix orders and Knuth-Bendix completion. Zbl 1356.68201
Sternagel, Christian; Thiemann, René
4
2011
Size-change termination for term rewriting. Zbl 1038.68072
Thiemann, René; Giesl, Jürgen
4
2003
Reachability analysis with state-compatible automata. Zbl 1362.68136
Felgenhauer, Bertram; Thiemann, René
3
2014
Formalizing bounded increase. Zbl 1317.68233
Thiemann, René
3
2013
From outermost termination to innermost termination. Zbl 1206.68094
Thiemann, René
3
2009
SAT solving for argument filterings. Zbl 1165.68484
Codish, Michael; Schneider-Kamp, Peter; Lagoon, Vitaly; Thiemann, René; Giesl, Jürgen
3
2006
A verified efficient implementation of the LLL basis reduction algorithm. Zbl 1409.68252
Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René
2
2018
A formalization of the LLL basis reduction algorithm. Zbl 06946979
Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa
2
2018
Generalized and formalized uncurrying. Zbl 1348.68086
Sternagel, Christian; Thiemann, René
2
2011
Deciding innermost loops. Zbl 1145.68457
Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter
2
2008
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 07187044
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 07176602
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
Certifying safety and termination proofs for integer transition systems. Zbl 06778420
Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2017
Reachability, confluence, and termination analysis with state-compatible automata. Zbl 1362.68137
Felgenhauer, Bertram; Thiemann, René
1
2017
Certification of complexity proofs using CeTA. Zbl 1366.68105
Avanzini, Martin; Sternagel, Christian; Thiemann, René
1
2015
A framework for developing stand-alone certifiers. Zbl 1342.68304
Sternagel, Christian; Thiemann, René
1
2015
Deriving comparators and show functions in Isabelle/HOL. Zbl 06481879
Sternagel, Christian; Thiemann, René
1
2015
Formalizing monotone algebras for certification of termination and complexity proofs. Zbl 1416.68180
Sternagel, Christian; Thiemann, René
1
2014
Certification of nontermination proofs. Zbl 1360.68767
Sternagel, Christian; Thiemann, René
1
2012
Certified subterm criterion and certified usable rules. Zbl 1236.68152
Sternagel, Christian; Thiemann, René
1
2010
Loops under strategies. Zbl 1242.68142
Thiemann, René; Sternagel, Christian
1
2009
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 07187044
Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 07176602
Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2020
A verified efficient implementation of the LLL basis reduction algorithm. Zbl 1409.68252
Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René
2
2018
A formalization of the LLL basis reduction algorithm. Zbl 06946979
Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa
2
2018
Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255
Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René
6
2017
Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 06821624
Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy
5
2017
Certifying safety and termination proofs for integer transition systems. Zbl 06778420
Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa
1
2017
Reachability, confluence, and termination analysis with state-compatible automata. Zbl 1362.68137
Felgenhauer, Bertram; Thiemann, René
1
2017
Algebraic numbers in Isabelle/HOL. Zbl 06644756
Thiemann, René; Yamada, Akihisa
5
2016
Termination Competition (termCOMP 2015). Zbl 06515500
Giesl, Jürgen; Mesnard, Frédéric; Rubio, Albert; Thiemann, René; Waldmann, Johannes
5
2015
Certification of complexity proofs using CeTA. Zbl 1366.68105
Avanzini, Martin; Sternagel, Christian; Thiemann, René
1
2015
A framework for developing stand-alone certifiers. Zbl 1342.68304
Sternagel, Christian; Thiemann, René
1
2015
Deriving comparators and show functions in Isabelle/HOL. Zbl 06481879
Sternagel, Christian; Thiemann, René
1
2015
Proving termination of programs automatically with AProVE. Zbl 1409.68256
Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René
13
2014
Reachability analysis with state-compatible automata. Zbl 1362.68136
Felgenhauer, Bertram; Thiemann, René
3
2014
Formalizing monotone algebras for certification of termination and complexity proofs. Zbl 1416.68180
Sternagel, Christian; Thiemann, René
1
2014
Formalizing bounded increase. Zbl 1317.68233
Thiemann, René
3
2013
SAT solving for termination proofs with recursive path orders and dependency pairs. Zbl 1276.68140
Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René
5
2012
Certification of nontermination proofs. Zbl 1360.68767
Sternagel, Christian; Thiemann, René
1
2012
Formalizing Knuth-Bendix orders and Knuth-Bendix completion. Zbl 1356.68201
Sternagel, Christian; Thiemann, René
4
2011
Generalized and formalized uncurrying. Zbl 1348.68086
Sternagel, Christian; Thiemann, René
2
2011
Automated termination analysis for logic programs with cut. Zbl 1209.68098
Schneider-Kamp, Peter; Giesl, Jürgen; Ströder, Thomas; Serebrenik, Alexander; Thiemann, René
8
2010
Signature extensions preserve termination. An alternative proof via dependency pairs. Zbl 1287.03032
Sternagel, Christian; Thiemann, René
5
2010
Certified subterm criterion and certified usable rules. Zbl 1236.68152
Sternagel, Christian; Thiemann, René
1
2010
Certification of termination proofs using CeTA. Zbl 1252.68265
Thiemann, René; Sternagel, Christian
25
2009
Automated termination proofs for logic programs by term rewriting. Zbl 1351.68054
Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René
11
2009
From outermost termination to innermost termination. Zbl 1206.68094
Thiemann, René
3
2009
Loops under strategies. Zbl 1242.68142
Thiemann, René; Sternagel, Christian
1
2009
Maximal termination. Zbl 1145.68446
Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald
8
2008
Improving context-sensitive dependency pairs. Zbl 1182.68092
Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René
6
2008
Deciding innermost loops. Zbl 1145.68457
Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter
2
2008
SAT solving for termination analysis with polynomial interpretations. Zbl 1214.68352
Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald
22
2007
Automated termination analysis for logic programs by term rewriting. Zbl 1196.68036
Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René
8
2007
Proving termination by bounded increase. Zbl 1213.68347
Giesl, Jürgen; Thiemann, René; Swiderski, Stephan; Schneider-Kamp, Peter
7
2007
Proving termination using recursive path orders and SAT solving. Zbl 1148.68393
Schneider-Kamp, Peter; Thiemann, René; Annov, Elena; Codish, Michael; Giesl, Jürgen
7
2007
Mechanizing and improving dependency pairs. Zbl 1113.68088
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
40
2006
Automated termination analysis for Haskell: from term rewriting to programming languages. Zbl 1151.68444
Giesl, Jürgen; Swiderski, Stephan; Schneider-Kamp, Peter; Thiemann, René
19
2006
SAT solving for argument filterings. Zbl 1165.68484
Codish, Michael; Schneider-Kamp, Peter; Lagoon, Vitaly; Thiemann, René; Giesl, Jürgen
3
2006
The dependency pair framework: Combining techniques for automated termination proofs. Zbl 1108.68477
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter
37
2005
Proving and disproving termination of higher-order functions. Zbl 1171.68714
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter
27
2005
The size-change principle and dependency pairs for termination of term rewriting. Zbl 1101.68640
Thiemann, René; Giesl, Jürgen
9
2005
Improved modular termination proofs using dependency pairs. Zbl 1126.68582
Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter
10
2004
Improving dependency pairs. Zbl 1273.68320
Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan
10
2003
Size-change termination for term rewriting. Zbl 1038.68072
Thiemann, René; Giesl, Jürgen
4
2003
all top 5

Cited by 181 Authors

19 Giesl, Jürgen
19 Lucas, Salvador
17 Thiemann, René
15 Middeldorp, Aart
12 Schneider-Kamp, Peter
9 Sternagel, Christian
8 Gutiérrez, Raúl
7 Fuhs, Carsten
7 Nishida, Naoki
7 Vidal, Germán
7 Zankl, Harald
7 Zantema, Hans
6 Endrullis, Jörg
6 Frohn, Florian
6 Hirokawa, Nao
6 Meseguer Guaita, José
6 Ströder, Thomas
6 Yamada, Akihisa
5 Hensel, Jera
5 Iborra, José
5 Winkler, Sarah
4 Ábrahám, Erika
4 Alarcón, Beatriz
4 Brockschmidt, Marc
4 Kremer, Gereon
3 Aschermann, Cornelius
3 Blanchette, Jasmin Christian
3 Borralleras, Cristina
3 Divasón, Jose
3 Emmes, Fabian
3 Falke, Stephan
3 Felgenhauer, Bertram
3 Gramlich, Bernhard
3 Greco, Sergio
3 Joosten, Sebastiaan J. C.
3 Lochbihler, Andreas
3 Rodríguez-Carbonell, Enric
3 Rubio, Albert
3 Sakai, Masahiko
3 Trubitsyna, Irina
2 Alpuente, María
2 Aoto, Takahito
2 Blanqui, Frédéric
2 Calautti, Marco
2 Codish, Michael
2 Corzilius, Florian
2 Cruz-Filipe, Luís
2 De Schreye, Danny
2 Drabent, Włodzimierz
2 Durán, Francisco
2 Escobar, Santiago
2 Fernández, Mirtha-Lina
2 Geuvers, Jan Herman
2 Hendriks, Dimitri
2 Kop, Cynthia
2 Korp, Martin
2 Krauss, Alexander
2 Molinaro, Cristian
2 Nagele, Julian
2 Navarro-Marset, Rafael
2 Nipkow, Tobias
2 Noschinski, Lars
2 Oliveras, Albert
2 Otto, Carsten
2 Parting, Michael
2 Paulson, Lawrence Charles
2 Plücker, Martin
2 Sabel, David
2 Schernhammer, Felix
2 Schlichtkrull, Anders
2 Swiderski, Stephan
2 Urbain, Xavier
2 Waldmann, Johannes
2 Waldmann, Uwe
1 Alkassar, Eyad
1 Andersen, Nils Byrial
1 Aransay, Jesús
1 Armstrong, Alasdair
1 Arroyo, Gustavo
1 Avanzini, Martin
1 Ayala-Rincón, Mauricio
1 Ben-Amram, Amir M.
1 Böhme, Sascha
1 Bottesch, Ralph Christian
1 Boudol, Gérard
1 Bulwahn, Lukas
1 Chan, Hing-Lun
1 Chihani, Zakaria
1 Comini, Marco
1 Coquand, Thierry
1 Courtieu, Pierre
1 De Vrijer, Roel C.
1 Deng, Yuxin
1 Falaschi, Moreno
1 Forest, Julien
1 Frittaion, Emanuele
1 Futatsugi, Kokichi
1 Galdino, André Luiz
1 Genet, Thomas
1 Gheri, Lorenzo
...and 81 more Authors

Citations by Year