Edit Profile (opens in new tab) Thiemann, René Compute Distance To: Compute Author ID: thiemann.rene Published as: Thiemann, René; Thiemann, Rene Documents Indexed: 56 Publications since 2003 2 Contributions as Editor Co-Authors: 54 Co-Authors with 55 Joint Publications 455 Co-Co-Authors all top 5 Co-Authors 3 single-authored 24 Giesl, Jürgen 20 Schneider-Kamp, Peter 15 Sternagel, Christian 7 Yamada, Akihisa 6 Fuhs, Carsten 5 Divasón, Jose 5 Joosten, Sebastiaan J. C. 3 Bottesch, Ralph Christian 3 Brockschmidt, Marc 3 Codish, Michael 3 Emmes, Fabian 3 Haslbeck, Max W. 3 Middeldorp, Aart 3 Serebrenik, Alexander 3 Ströder, Thomas 2 Falke, Stephan 2 Felgenhauer, Bertram 2 Frohn, Florian 2 Otto, Carsten 2 Plücker, Martin 2 Swiderski, Stephan 2 Swiderski, Stephanie 2 Zankl, Harald 1 Alarcón, Beatriz 1 Allais, Guillaume 1 Annov, Elena 1 Aschermann, Cornelius 1 Avanzini, Martin 1 Benevides, Mario R. F. 1 Biendarra, Julian 1 Blanchette, Jasmin Christian 1 Bouzy, Aymeric 1 Desharnais, Martin 1 Fleury, Mathias 1 Gutiérrez, Raúl 1 Hensel, Jera 1 Hölzl, Johannes 1 Krauss, Alexander 1 Kunčar, Ondřej 1 Kusakari, Keiichirou 1 Lagoon, Vitaly 1 Lochbihler, Andreas 1 Lucas, Salvador 1 Meier, Fabian 1 Mesnard, Frédéric 1 Nagele, Julian 1 Nigam, Vivek 1 Panny, Lorenz 1 Popescu, Andrei 1 Rubio, Albert 1 Traytel, Dmitry 1 Waldmann, Johannes 1 Winkler, Sarah 1 Zantema, Hans all top 5 Serials 8 Journal of Automated Reasoning 2 Applicable Algebra in Engineering, Communication and Computing 1 Theoretical Computer Science 1 Information and Computation 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 1 Electronic Notes in Theoretical Computer Science 1 Journal of Logical and Algebraic Methods in Programming all top 5 Fields 58 Computer science (68-XX) 7 Mathematical logic and foundations (03-XX) 4 Number theory (11-XX) 3 Commutative algebra (13-XX) 2 General and overarching topics; collections (00-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 47 Publications have been cited 421 times in 199 Documents Cited by ▼ Year ▼ Mechanizing and improving dependency pairs. Zbl 1113.68088Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 52 2006 The dependency pair framework: Combining techniques for automated termination proofs. Zbl 1108.68477Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter 41 2005 Certification of termination proofs using CeTA. Zbl 1252.68265Thiemann, René; Sternagel, Christian 30 2009 Proving and disproving termination of higher-order functions. Zbl 1171.68714Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter 28 2005 SAT solving for termination analysis with polynomial interpretations. Zbl 1214.68352Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald 24 2007 Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255Giesl, 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é 21 2017 Automated termination analysis for Haskell: from term rewriting to programming languages. Zbl 1151.68444Giesl, Jürgen; Swiderski, Stephan; Schneider-Kamp, Peter; Thiemann, René 20 2006 Proving termination of programs automatically with AProVE. Zbl 1409.68256Giesl, 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é 20 2014 Automated termination proofs for logic programs by term rewriting. Zbl 1351.68054Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René 13 2009 Maximal termination. Zbl 1145.68446Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald 11 2008 Improved modular termination proofs using dependency pairs. Zbl 1126.68582Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter 10 2004 Automated termination analysis for logic programs with cut. Zbl 1209.68098Schneider-Kamp, Peter; Giesl, Jürgen; Ströder, Thomas; Serebrenik, Alexander; Thiemann, René 10 2010 The size-change principle and dependency pairs for termination of term rewriting. Zbl 1101.68640Thiemann, René; Giesl, Jürgen 10 2005 Automated termination analysis for logic programs by term rewriting. Zbl 1196.68036Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René 8 2007 Improving context-sensitive dependency pairs. Zbl 1182.68092Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René 8 2008 Proving termination using recursive path orders and SAT solving. Zbl 1148.68393Schneider-Kamp, Peter; Thiemann, René; Annov, Elena; Codish, Michael; Giesl, Jürgen 7 2007 Proving termination by bounded increase. Zbl 1213.68347Giesl, Jürgen; Thiemann, René; Swiderski, Stephan; Schneider-Kamp, Peter 7 2007 Improving dependency pairs. Zbl 1273.68320Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 7 2003 Signature extensions preserve termination. An alternative proof via dependency pairs. Zbl 1287.03032Sternagel, Christian; Thiemann, René 7 2010 Algebraic numbers in Isabelle/HOL. Zbl 1478.68443Thiemann, René; Yamada, Akihisa 6 2016 Termination Competition (termCOMP 2015). Zbl 1465.68282Giesl, Jürgen; Mesnard, Frédéric; Rubio, Albert; Thiemann, René; Waldmann, Johannes 6 2015 Formalizing monotone algebras for certification of termination and complexity proofs. Zbl 1416.68180Sternagel, Christian; Thiemann, René 6 2014 SAT solving for termination proofs with recursive path orders and dependency pairs. Zbl 1276.68140Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René 6 2012 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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 6 2017 Formalizing Knuth-Bendix orders and Knuth-Bendix completion. Zbl 1356.68201Sternagel, Christian; Thiemann, René 5 2011 Size-change termination for term rewriting. Zbl 1038.68072Thiemann, René; Giesl, Jürgen 4 2003 A verified efficient implementation of the LLL basis reduction algorithm. Zbl 1409.68252Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René 4 2018 A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 1469.68165Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 4 2020 Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. Zbl 1435.68362Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René 4 2019 From outermost termination to innermost termination. Zbl 1206.68094Thiemann, René 3 2009 A formalization of the LLL basis reduction algorithm. Zbl 1468.68287Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa 3 2018 Reachability analysis with state-compatible automata. Zbl 1362.68136Felgenhauer, Bertram; Thiemann, René 3 2014 AC dependency pairs revisited. Zbl 1369.68250Yamada, Akihisa; Sternagel, Christian; Thiemann, René; Kusakari, Keiichirou 3 2016 Formalizing bounded increase. Zbl 1317.68233Thiemann, René 3 2013 SAT solving for argument filterings. Zbl 1165.68484Codish, Michael; Schneider-Kamp, Peter; Lagoon, Vitaly; Thiemann, René; Giesl, Jürgen 3 2006 Reachability, confluence, and termination analysis with state-compatible automata. Zbl 1362.68137Felgenhauer, Bertram; Thiemann, René 3 2017 Deriving comparators and show functions in Isabelle/HOL. Zbl 1465.68063Sternagel, Christian; Thiemann, René 2 2015 Deciding innermost loops. Zbl 1145.68457Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter 2 2008 A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 1468.68326Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 2 2020 Generalized and formalized uncurrying. Zbl 1348.68086Sternagel, Christian; Thiemann, René 2 2011 Loops under strategies. Zbl 1242.68142Thiemann, René; Sternagel, Christian 1 2009 Modular and certified semantic labeling and unlabeling. Zbl 1236.68151Sternagel, Christian; Thiemann, René 1 2011 Certified subterm criterion and certified usable rules. Zbl 1236.68152Sternagel, Christian; Thiemann, René 1 2010 A framework for developing stand-alone certifiers. Zbl 1342.68304Sternagel, Christian; Thiemann, René 1 2015 Certification of complexity proofs using CeTA. Zbl 1366.68105Avanzini, Martin; Sternagel, Christian; Thiemann, René 1 2015 Certifying safety and termination proofs for integer transition systems. Zbl 1494.68294Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 1 2017 Certification of nontermination proofs. Zbl 1360.68767Sternagel, Christian; Thiemann, René 1 2012 A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. Zbl 1469.68165Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 4 2020 A verified implementation of algebraic numbers in Isabelle/HOL. Zbl 1468.68326Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 2 2020 Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. Zbl 1435.68362Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René 4 2019 A verified efficient implementation of the LLL basis reduction algorithm. Zbl 1409.68252Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René 4 2018 A formalization of the LLL basis reduction algorithm. Zbl 1468.68287Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa 3 2018 Analyzing program termination and complexity automatically with AProVE. Zbl 1409.68255Giesl, 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é 21 2017 Foundational (co)datatypes and (co)recursion for higher-order logic. Zbl 1495.68238Biendarra, 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 6 2017 Reachability, confluence, and termination analysis with state-compatible automata. Zbl 1362.68137Felgenhauer, Bertram; Thiemann, René 3 2017 Certifying safety and termination proofs for integer transition systems. Zbl 1494.68294Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa 1 2017 Algebraic numbers in Isabelle/HOL. Zbl 1478.68443Thiemann, René; Yamada, Akihisa 6 2016 AC dependency pairs revisited. Zbl 1369.68250Yamada, Akihisa; Sternagel, Christian; Thiemann, René; Kusakari, Keiichirou 3 2016 Termination Competition (termCOMP 2015). Zbl 1465.68282Giesl, Jürgen; Mesnard, Frédéric; Rubio, Albert; Thiemann, René; Waldmann, Johannes 6 2015 Deriving comparators and show functions in Isabelle/HOL. Zbl 1465.68063Sternagel, Christian; Thiemann, René 2 2015 A framework for developing stand-alone certifiers. Zbl 1342.68304Sternagel, Christian; Thiemann, René 1 2015 Certification of complexity proofs using CeTA. Zbl 1366.68105Avanzini, Martin; Sternagel, Christian; Thiemann, René 1 2015 Proving termination of programs automatically with AProVE. Zbl 1409.68256Giesl, 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é 20 2014 Formalizing monotone algebras for certification of termination and complexity proofs. Zbl 1416.68180Sternagel, Christian; Thiemann, René 6 2014 Reachability analysis with state-compatible automata. Zbl 1362.68136Felgenhauer, Bertram; Thiemann, René 3 2014 Formalizing bounded increase. Zbl 1317.68233Thiemann, René 3 2013 SAT solving for termination proofs with recursive path orders and dependency pairs. Zbl 1276.68140Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René 6 2012 Certification of nontermination proofs. Zbl 1360.68767Sternagel, Christian; Thiemann, René 1 2012 Formalizing Knuth-Bendix orders and Knuth-Bendix completion. Zbl 1356.68201Sternagel, Christian; Thiemann, René 5 2011 Generalized and formalized uncurrying. Zbl 1348.68086Sternagel, Christian; Thiemann, René 2 2011 Modular and certified semantic labeling and unlabeling. Zbl 1236.68151Sternagel, Christian; Thiemann, René 1 2011 Automated termination analysis for logic programs with cut. Zbl 1209.68098Schneider-Kamp, Peter; Giesl, Jürgen; Ströder, Thomas; Serebrenik, Alexander; Thiemann, René 10 2010 Signature extensions preserve termination. An alternative proof via dependency pairs. Zbl 1287.03032Sternagel, Christian; Thiemann, René 7 2010 Certified subterm criterion and certified usable rules. Zbl 1236.68152Sternagel, Christian; Thiemann, René 1 2010 Certification of termination proofs using CeTA. Zbl 1252.68265Thiemann, René; Sternagel, Christian 30 2009 Automated termination proofs for logic programs by term rewriting. Zbl 1351.68054Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René 13 2009 From outermost termination to innermost termination. Zbl 1206.68094Thiemann, René 3 2009 Loops under strategies. Zbl 1242.68142Thiemann, René; Sternagel, Christian 1 2009 Maximal termination. Zbl 1145.68446Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald 11 2008 Improving context-sensitive dependency pairs. Zbl 1182.68092Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René 8 2008 Deciding innermost loops. Zbl 1145.68457Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter 2 2008 SAT solving for termination analysis with polynomial interpretations. Zbl 1214.68352Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald 24 2007 Automated termination analysis for logic programs by term rewriting. Zbl 1196.68036Schneider-Kamp, Peter; Giesl, Jürgen; Serebrenik, Alexander; Thiemann, René 8 2007 Proving termination using recursive path orders and SAT solving. Zbl 1148.68393Schneider-Kamp, Peter; Thiemann, René; Annov, Elena; Codish, Michael; Giesl, Jürgen 7 2007 Proving termination by bounded increase. Zbl 1213.68347Giesl, Jürgen; Thiemann, René; Swiderski, Stephan; Schneider-Kamp, Peter 7 2007 Mechanizing and improving dependency pairs. Zbl 1113.68088Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 52 2006 Automated termination analysis for Haskell: from term rewriting to programming languages. Zbl 1151.68444Giesl, Jürgen; Swiderski, Stephan; Schneider-Kamp, Peter; Thiemann, René 20 2006 SAT solving for argument filterings. Zbl 1165.68484Codish, 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.68477Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter 41 2005 Proving and disproving termination of higher-order functions. Zbl 1171.68714Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter 28 2005 The size-change principle and dependency pairs for termination of term rewriting. Zbl 1101.68640Thiemann, René; Giesl, Jürgen 10 2005 Improved modular termination proofs using dependency pairs. Zbl 1126.68582Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter 10 2004 Improving dependency pairs. Zbl 1273.68320Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan 7 2003 Size-change termination for term rewriting. Zbl 1038.68072Thiemann, René; Giesl, Jürgen 4 2003 all cited Publications top 5 cited Publications all top 5 Cited by 257 Authors 24 Lucas, Salvador 20 Giesl, Jürgen 19 Thiemann, René 18 Middeldorp, Aart 12 Schneider-Kamp, Peter 11 Gutiérrez, Raúl 11 Nishida, Naoki 10 Sternagel, Christian 9 Yamada, Akihisa 8 Winkler, Sarah 8 Zankl, Harald 7 Fuhs, Carsten 7 Vidal, Germán 7 Zantema, Hans 6 Endrullis, Jörg 6 Frohn, Florian 6 Hirokawa, Nao 6 Meseguer Guaita, José 6 Ströder, Thomas 5 Hensel, Jera 5 Iborra, José 5 Kremer, Gereon 5 Moser, Georg 5 Nipkow, Tobias 4 Ábrahám, Erika 4 Alarcón, Beatriz 4 Brockschmidt, Marc 4 Divasón, Jose 4 Felgenhauer, Bertram 3 Aschermann, Cornelius 3 Blanchette, Jasmin Christian 3 Blanqui, Frédéric 3 Borralleras, Cristina 3 Cimatti, Alessandro 3 Emmes, Fabian 3 Falke, Stephan 3 Gramlich, Bernhard 3 Greco, Sergio 3 Griggio, Alberto 3 Joosten, Sebastiaan J. C. 3 Lochbihler, Andreas 3 Rodríguez-Carbonell, Enric 3 Rubio, Albert 3 Sakai, Masahiko 3 Trubitsyna, Irina 3 Waldmann, Johannes 2 Allamigeon, Xavier 2 Alpuente, María 2 Aoto, Takahito 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 Eßmann, Robin 2 Fernández, Mirtha-Lina 2 Geuvers, Jan Herman 2 Hendriks, Dimitri 2 Katz, Ricardo David 2 Kop, Cynthia 2 Korp, Martin 2 Krauss, Alexander 2 Leutgeb, Lorenz 2 Lochmann, Alexander 2 Magnago, Enrico 2 Mehlhorn, Kurt 2 Molinaro, Cristian 2 Nagele, Julian 2 Navarro-Marset, Rafael 2 Noschinski, Lars 2 Oliveras, Albert 2 Otto, Carsten 2 Parting, Michael 2 Paulson, Lawrence Charles 2 Plücker, Martin 2 Robillard, Simon 2 Sabel, David 2 Schernhammer, Felix 2 Schlichtkrull, Anders 2 Strub, Pierre-Yves 2 Swiderski, Stephan 2 Urbain, Xavier 2 Waldmann, Uwe 2 Zhang, Shujun 2 Zuleger, Florian 1 Aaronson, Scott 1 Abdulaziz, Mohammad 1 Albert, Elvira 1 Alkassar, Eyad 1 Aransay, Jesús 1 Armstrong, Alasdair 1 Arroyo, Gustavo 1 Avanzini, Martin 1 Avigad, Jeremy 1 Ayala-Rincón, Mauricio 1 Barbosa, Haniel 1 Barrett, Clark W. ...and 157 more Authors all top 5 Cited in 21 Serials 36 Journal of Automated Reasoning 10 Information and Computation 8 Journal of Logical and Algebraic Methods in Programming 6 Applicable Algebra in Engineering, Communication and Computing 6 Logical Methods in Computer Science 5 Theoretical Computer Science 5 Formal Aspects of Computing 5 Theory and Practice of Logic Programming 4 Information Processing Letters 3 MSCS. Mathematical Structures in Computer Science 2 Journal of Symbolic Computation 2 Annals of Mathematics and Artificial Intelligence 2 The Journal of Logic and Algebraic Programming 2 ACM Transactions on Computational Logic 1 Acta Informatica 1 Journal of Computer and System Sciences 1 Distributed Computing 1 Journal of Functional Programming 1 Higher-Order and Symbolic Computation 1 RAIRO. Theoretical Informatics and Applications 1 Acta Universitatis Sapientiae. Informatica all top 5 Cited in 11 Fields 196 Computer science (68-XX) 32 Mathematical logic and foundations (03-XX) 4 Field theory and polynomials (12-XX) 3 Number theory (11-XX) 2 Combinatorics (05-XX) 2 Order, lattices, ordered algebraic structures (06-XX) 2 Commutative algebra (13-XX) 2 Operations research, mathematical programming (90-XX) 1 Algebraic geometry (14-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year