Computational Logic Department of Computer Science University of Innsbruck
assoc. Prof. Dr. René Thiemann 
Department of Computer Science
Computational Logic Group
University of Innsbruck
Techniker Str. 21a
A-6020 Innsbruck
Austria

E-Mail: rene._mylastname_@uibk.ac.at
Phone: +43/512/507 53234
Room: 3M09, 2. OG
Office hours: Monday 13:00h - 15:00h
René Thiemann

Research

I am an assistant professor at the Computational Logic group and project leader of the FWF projects

My fields of interest include but are not limited to:

Upcoming events

Teaching Activities

Publications

Theses

Journals

Conferences

  1. J. Biendarra, J. Blanchette, A. Bouzy, M. Desharnais, M. Fleury, J. Hölzl, O. Kunčar, A. Lochbihler, F. Meier, L. Panny, A. Popescu, C. Sternagel, R. Thiemann, D. Traytel.
    Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
    In Proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS '17), Lecture Notes in Computer Science 10483, pages 3-21, 2017.

  2. M. Brockschmidt, S. Joosten, R. Thiemann and A. Yamada.
    Certifying Safety and Termination Proofs for Integer Transition Systems
    In Proceedings of the 26th International Conference on Automated Deduction (CADE '17), Lecture Notes in Computer Science 10395, pages 454-471, 2017.

  3. J. Divasón, S. Joosten, R. Thiemann and A. Yamada.
    A Formalization of the Berlekamp–Zassenhaus Factorization Algorithm
    In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '17), pages 17-29, 2017.

  4. Akihisa Yamada, C. Sternagel, R. Thieman, and K. Kusakari
    AC Dependency Pairs Revisited
    In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL '16), Leibniz International Proceedings in Informatics 62, pages 8:1-8:16, 2016.

  5. R. Thiemann and A. Yamada.
    Algebraic Numbers in Isabelle/HOL
    In Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP '16), Lecture Notes in Computer Science 9807, pages 391-408, 2016.

  6. R. Thiemann and A. Yamada.
    Formalizing Jordan Normal Forms in Isabelle/HOL
    In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '16), pages 88-99, 2016.

  7. S. Winkler and R. Thiemann.
    Formalizing Soundness and Completeness of Unravelings
    In Proceedings of the 10th International Symposium on Frontiers of Combining Systems (FroCoS '15), Lecture Notes in Artificial Intelligence 9322, pages 239-255, 2015.

  8. C. Sternagel and R. Thiemann.
    Deriving Comparators and Show Functions in Isabelle/HOL
    In Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP '15), Lecture Notes in Computer Science 9236, pages 421-437, 2015.

  9. M. Avanzini, C. Sternagel, and R. Thiemann
    Certification of Complexity Proofs using CeTA
    In Proceedings of the Joint 26th International Conference on Rewriting Techniques and Applications (RTA '15), Leibniz International Proceedings in Informatics 36, pages 23-39, 2015.

  10. J. Nagele, R. Thiemann, and S. Winkler
    Certification of Nontermination Proofs using Strategies and Nonlooping Derivations
    In Proceedings of the 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '14), Lecture Notes in Computer Science, 8471, pages 216-232, 2014, © Springer-Verlag.

  11. C. Sternagel and R. Thiemann
    The Certification Problem Format
    In Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP '14), Electronic Proceedings in Theoretical Computer Science 167:61-72, 2014.

  12. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
    Proving Termination of Programs Automatically with AProVE
    In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Lecture Notes in Computer Science, 8562, pages 184-191, 2014, © Springer-Verlag.

  13. C. Sternagel and R. Thiemann
    Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
    In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA '14), Lecture Notes in Computer Science 8560 (Advanced Research in Computing and Software Science), pages 441-455, 2014, © Springer-Verlag.

  14. B. Felgenhauer and R. Thiemann.
    Reachability Analysis with State-Compatible Automata
    In Proceedings of 8th International Conference on Language and Automata Theory and Applications (LATA '14), Lecture Notes in Computer Science 8370, pages 347-359, 2014, © Springer-Verlag.

  15. R. Thiemann.
    Formalizing Bounded Increase
    In Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP '13), Lecture Notes in Computer Science 7998, pages 245-260, 2013, © Springer-Verlag.

  16. C. Sternagel and R. Thiemann.
    Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
    In Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA '13), Leibniz International Proceedings in Informatics 21:287-302, 2013.

  17. C. Sternagel and R. Thiemann.
    Certification of Nontermination Proofs
    In Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP '12), Lecture Notes in Computer Science 7406, pages 266-282, 2012, © Springer-Verlag.

  18. R. Thiemann, G. Allais, and J. Nagele.
    On the formalization of termination techniques based on multiset orderings
    In Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12), Leibniz International Proceedings in Informatics 15:339-354, 2012.

  19. C. Sternagel and R. Thiemann.
    Generalized and Formalized Uncurrying
    In Proceedings of the 8th International Symposium Frontiers of Combining Systems (FroCoS '11), Lecture Notes in Artificial Intelligence 6989, pages 243-258, 2011. © Springer-Verlag.

  20. A. Krauss, C. Sternagel, R. Thiemann, C. Fuhs, and J. Giesl.
    Termination of Isabelle Functions via Termination of Rewriting
    In Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP '11), Lecture Notes in Computer Science 6898, pages 152-167, 2011. © Springer-Verlag.

  21. C. Sternagel and R. Thiemann
    Modular and certified semantic labeling and unlabeling
    In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11), Leibniz International Proceedings in Informatics 10:329-344, 2011.

  22. R. Thiemann, C. Sternagel, J. Giesl, and P. Schneider-Kamp
    Loops under Strategies ... Continued
    In Proceedings of the International Workshop on Strategies in Rewriting, Proving, and Programming, Electronic Proceedings in Theoretical Computer Science 44:51-65, 2010.

  23. C. Sternagel and R. Thiemann
    Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
    In Proceedings of the 19th EACSL Annual Conferences on Computer Science Logic (CSL '10), Lecture Notes in Computer Science 6247, pages 514-528, 2010. © Springer-Verlag.

  24. P. Schneider-Kamp, J. Giesl, T. Ströder, A. Serebrenik, and R. Thiemann
    Automated termination analysis for logic programs with cut
    In Proceedings of the 26th International Conference on Logic Programming (ICLP '10), Theory and Practice of Logic Programming 10(4-6):365-381, 2010.
    Cambridge University Press.
    Extended version appeared as Technical Report AIB-2010-10, RWTH Aachen, Germany.

  25. C. Sternagel and R. Thiemann
    Certified Subterm Criterion and Certified Usable Rules
    In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10), Leibniz International Proceedings in Informatics 6:325-340, 2010.

  26. R. Thiemann and C. Sternagel
    Certification of Termination Proofs using CeTA
    In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09), Lecture Notes in Computer Science 5674, pages 452-468, 2009. © Springer-Verlag.

  27. R. Thiemann and C. Sternagel
    Loops under Strategies
    In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Lecture Notes in Computer Science 5595, pages 17-31, 2009. © Springer-Verlag.
    All proofs are available in this extended version.

  28. R. Thiemann
    From outermost termination to innermost termination
    In Proceedings of the 35th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM '09), Spindleruv Mlyn, Czech Republic. Lecture Notes in Computer Science 5404, pages 533-545, 2009. © Springer-Verlag

  29. B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann
    Improving Context-Sensitive Dependency Pairs
    In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, Lecture Notes in Computer Science 5330, pages 636-651, 2008. © Springer-Verlag.
    Extended version available as Technical Report AIB-2008-13, RWTH Aachen, Germany.

  30. R. Thiemann, J. Giesl, and P. Schneider-Kamp
    Deciding Innermost Loops
    In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 366-380, 2008. © Springer-Verlag

  31. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
    Maximal Termination
    In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, Lecture Notes in Computer Science 5117, pages 110-125, 2008. © Springer-Verlag
    Extended version available as Technical Report AIB-2008-03, RWTH Aachen, Germany.

  32. R. Thiemann and A. Middeldorp
    Innermost Termination of Rewrite Systems by Labeling
    In Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '07), Paris, France, Electronic Notes in Theoretical Computer Science 204 (2008), pages 3-19, 2008. © Elsevier.
    Original publication available at Science Direct.

  33. P. Schneider-Kamp, R. Thiemann, E. Annov, M. Codish, and J. Giesl
    Proving Termination using Recursive Path Orders and SAT Solving
    In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS '07), Liverpool, UK, Lecture Notes in Artificial Intelligence 4720, pages 267-282, 2007. © Springer-Verlag

  34. J. Giesl, R. Thiemann, S. Swiderski, and P. Schneider-Kamp
    Proving Termination by Bounded Increase
    In Proceedings of the 21st Conference on Automated Deduction (CADE '07), Bremen, Germany, Lecture Notes in Artificial Intelligence 4603, pages 443-459, 2007. ©Springer-Verlag

  35. C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
    SAT Solving for Termination Analysis with Polynomial Interpretations
    In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT '07), Lisbon, Portugal, Lecture Notes in Computer Science 4501, pages 340-354, 2007. ©Springer-Verlag

  36. P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
    Automated Termination Analysis for Logic Programs by Term Rewriting
    In Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '06), Venice, Italy, Lecture Notes in Computer Science 4407, pages 177-193, 2006. ©Springer-Verlag

  37. M. Codish, P. Schneider-Kamp, V. Lagoon, R. Thiemann, and J. Giesl
    SAT Solving for Argument Filterings
    In Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '06), Phnom Penh, Cambodia, Lecture Notes in Artificial Intelligence 4246, pages 30-44, 2006. © Springer-Verlag

  38. J. Giesl, P. Schneider-Kamp, and R. Thiemann
    AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework
    In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06), Seattle, USA, Lecture Notes in Artificial Intelligence 4130, pages 281-286, 2006. ©Springer-Verlag

  39. J. Giesl, S. Swiderski, P. Schneider-Kamp, and R. Thiemann
    Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
    In Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA '06), Seattle, USA, Lecture Notes in Computer Science 4098, pages 297-312, 2006. ©Springer-Verlag

  40. J. Giesl, R. Thiemann, and P. Schneider-Kamp
    Proving and Disproving Termination of Higher-Order Functions
    In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05), Vienna, Austria, Lecture Notes in Artificial Intelligence 3717, pages 216-231, 2005. © Springer-Verlag

  41. J. Giesl, R. Thiemann, and P. Schneider-Kamp
    The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
    In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '04), Montevideo, Uruguay, Lecture Notes in Artificial Intelligence 3452, pages 301-331, 2005. © Springer-Verlag

  42. R. Thiemann, J. Giesl, and P. Schneider-Kamp
    Improved Modular Termination Proofs Using Dependency Pairs
    In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR '04), Cork, Ireland, Lecture Notes in Artificial Intelligence 3097, pages 75-90, 2004. © Springer-Verlag

  43. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
    Automated Termination Proofs with AProVE
    In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA '04), Aachen, Germany, Lecture Notes in Computer Science 3091, pages 210-220, 2004. © Springer-Verlag

  44. J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
    Improving Dependency Pairs
    In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '03), Almaty, Kazakhstan, Lecture Notes in Artificial Intelligence 2850, pages 167-182, 2003. ©Springer-Verlag
    Extended version available as Technical Report AIB-2003-04, RWTH Aachen, Germany.

  45. R. Thiemann and J. Giesl
    Size-Change Termination for Term Rewriting
    In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA '03), Valencia, Spain, Lecture Notes in Computer Science 2706, pages 264-278, 2003. ©Springer-Verlag
    Extended version available as Technical Report AIB-2003-02, RWTH Aachen, Germany.

Miscellaneous