Ren Thiemann
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
35
Venues
12
Active years
2003–2026
Best venue rank
A*
Where they publish
Papers
35 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | FSCD | New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations. | Ren Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann |
| 2026 | IJCAR | The ARI Infrastructure for Automated Confluence Analysis. | Nao Hirokawa, Aart Middeldorp, Teppei Saito, Ren Thiemann |
| 2025 | CPP | An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. | Dohan Kim, Teppei Saito, Ren Thiemann, Akihisa Yamada |
| 2024 | CPP | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. | Nao Hirokawa, Dohan Kim, Kiraku Shintani, Ren Thiemann |
| 2024 | FSCD | A Verified Algorithm for Deciding Pattern Completeness. | Ren Thiemann, Akihisa Yamada |
| 2024 | LICS | Linear Termination is Undecidable. | Fabian Mitterwallner, Aart Middeldorp, Ren Thiemann |
| 2021 | CPP | An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. | Max W. Haslbeck, Ren Thiemann |
| 2020 | FSCD | Certifying the Weighted Path Order (Invited Talk). | Ren Thiemann, Jonas Schpf, Christian Sternagel, Akihisa Yamada |
| 2018 | CPP | Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). | Jose Divasn, Sebastiaan J. C. Joosten, Ondrej Kuncar, Ren Thiemann, Akihisa Yamada |
| 2018 | ITP | A Formalization of the LLL Basis Reduction Algorithm. | Jose Divasn, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2018 | LPAR | A Verified Efficient Implementation of the LLL Basis Reduction Algorithm. | Ralph Bottesch, Max W. Haslbeck, Ren Thiemann |
| 2018 | LPAR | Extending a Verified Simplex Algorithm. | Ren Thiemann |
| 2017 | CADE | Certifying Safety and Termination Proofs for Integer Transition Systems. | Marc Brockschmidt, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2017 | CPP | A formalization of the Berlekamp-Zassenhaus factorization algorithm. | Jose Divasn, Sebastiaan J. C. Joosten, Ren Thiemann, Akihisa Yamada |
| 2016 | CPP | Formalizing jordan normal forms in Isabelle/HOL. | Ren Thiemann, Akihisa Yamada |
| 2016 | CSL | AC Dependency Pairs Revisited. | Akihisa Yamada, Christian Sternagel, Ren Thiemann, Keiichirou Kusakari |
| 2016 | ITP | Algebraic Numbers in Isabelle/HOL. | Ren Thiemann, Akihisa Yamada |
| 2015 | CADE | Termination Competition (termCOMP 2015). | Jrgen Giesl, Frdric Mesnard, Albert Rubio, Ren Thiemann, Johannes Waldmann |
| 2015 | ITP | Deriving Comparators and Show Functions in Isabelle/HOL. | Christian Sternagel, Ren Thiemann |
| 2014 | CADE | Proving Termination of Programs Automatically with AProVE. | Jrgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plcker, Peter Schneider-Kamp, Thomas Strder, Stephanie Swiderski, Ren Thiemann |
| 2014 | LATA | Reachability Analysis with State-Compatible Automata. | Bertram Felgenhauer, Ren Thiemann |
| 2013 | ITP | Formalizing Bounded Increase. | Ren Thiemann |
| 2012 | ITP | Certification of Nontermination Proofs. | Christian Sternagel, Ren Thiemann |
| 2011 | ITP | Termination of Isabelle Functions via Termination of Rewriting. | Alexander Krauss, Christian Sternagel, Ren Thiemann, Carsten Fuhs, Jrgen Giesl |
| 2010 | CSL | Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. | Christian Sternagel, Ren Thiemann |
| 2009 | SOFSEM | From Outermost Termination to Innermost Termination. | Ren Thiemann |
| 2008 | LPAR | Improving Context-Sensitive Dependency Pairs. | Beatriz Alarcn, Fabian Emmes, Carsten Fuhs, Jrgen Giesl, Ral Gutirrez, Salvador Lucas, Peter Schneider-Kamp, Ren Thiemann |
| 2007 | CADE | Proving Termination by Bounded Increase. | Jrgen Giesl, Ren Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
| 2007 | SAT | SAT Solving for Termination Analysis with Polynomial Interpretations. | Carsten Fuhs, Jrgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren Thiemann, Harald Zankl |
| 2006 | CADE | Automatic Termination Proofs in the Dependency Pair Framework. | Jrgen Giesl, Peter Schneider-Kamp, Ren Thiemann |
| 2006 | LOPSTR | Automated Termination Analysis for Logic Programs by Term Rewriting. | Peter Schneider-Kamp, Jrgen Giesl, Alexander Serebrenik, Ren Thiemann |
| 2006 | LPAR | SAT Solving for Argument Filterings. | Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, Ren Thiemann, Jrgen Giesl |
| 2004 | CADE | Improved Modular Termination Proofs Using Dependency Pairs. | Ren Thiemann, Jrgen Giesl, Peter Schneider-Kamp |
| 2004 | LPAR | The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp |
| 2003 | LPAR | Improving Dependency Pairs. | Jrgen Giesl, Ren Thiemann, Peter Schneider-Kamp, Stephan Falke |