Research

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

• Improving Certifiers for Termination Proofs and
• Certifying Termination and Complexity Proofs of Programs.

My fields of interest include but are not limited to:

• Interactive theorem proving (IsaFoR / CeTA, certification problem format, Isabelle, and Archive of Formal Proofs)
• Termination analysis (tools AProVE and TTT2, and termination portal)
• Term rewriting
• SAT and SMT solving
• Algebra, in particular algebraic numbers and related algorithms

Upcoming events

• 14th International School on Rewriting (ISR 2024), August 25 – September 1, 2024

Teaching Activities

• Lecture and Proseminar Functional Programming (WS 24/25)
• Lecture Advanced Functional Programming (WS 24/25)
• Lecture and Proseminar Program Verification (SS 24)
• Lecture Interactive Theorem Proving in Isabelle/HOL (SS 24)
• Lecture Constraint Solving (SS 24)
• Lecture and Proseminar Functional Programming (WS 23/24)
• Lecture and Proseminar Program Verification (SS 23)
• Lecture Interactive Theorem Proving in Isabelle/HOL (SS 23)
• Lecture and Proseminar Functional Programming (WS 22/23)
• Lecture Constraint Solving (WS 22/23)
• Lecture Interactive Theorem Proving in Isabelle/HOL (SS 22)
• Lecture and Proseminar Program Verification (SS 22)
• Lecture and Proseminar Functional Programming (WS 21/22)
• Lecture and Proseminar Constraint Solving (WS 21/22)
• Lecture and Proseminar Program Verification (SS 21)
• Lecture Decision Procedures (SS 21)
• Lecture and Proseminar Functional Programming (WS 20/21)
• Lecture and Proseminar Program Verification (SS 20)
• Lecture and Proseminar Functional Programming (WS 19/20)
• ... several courses before 2019 ...

Publications

Theses

• Habilitation thesis
  A Formalization of Termination Techniques in Isabelle/HOL
  January 2013. University of Innsbruck, Austria.

• PhD thesis
  The DP Framework for Proving Termination of Term Rewriting
  October 2007. Available as Technical Report AIB-2007-17, RWTH Aachen University, Germany. In this revised version some typos have been fixed.

Journals

• R. Thiemann
  A Perron–Frobenius Theorem for Deciding Matrix Growth
  Journal of Logical and Algebraic Methods in Programming, 123, November 2021.

• R. Thiemann, R. Bottesch, J. Divasón, M. Haslbeck, S. Joosten, and A. Yamada
  Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
  Journal of Automated Reasoning, 64:827-856, 2020.

• J. Divasón, S. Joosten, R. Thiemann, and A. Yamada
  A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm
  Journal of Automated Reasoning, 64:699-735, 2020.

• S. Joosten, R. Thiemann, and A. Yamada
  A Verified Implementation of Algebraic Numbers in Isabelle/HOL
  Journal of Automated Reasoning, 64:363-389, 2020.

• J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
  Analyzing Program Termination and Complexity Automatically with AProVE
  Journal of Automated Reasoning, 58(1):3-31, 2017. © Springer-Verlag
  Preliminary version (The final publication is available at Springer)

• B. Felgenhauer and R. Thiemann
  Reachability, confluence, and termination analysis with state-compatible automata
  Information and Computation, 253(3):467-483, 2017.

• C. Sternagel and R. Thiemann
  A Framework for Developing Stand-Alone Certifiers
  Electronic Notes in Theoretical Computer Science, 312:51-67, 2015.

• M. Codish, J. Giesl, P. Schneider-Kamp, and R. Thiemann
  SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
  Journal of Automated Reasoning, 49(1):53-93, 2012. © Springer-Verlag
  Preliminary version (The final publication is available at www.springerlink.com)

• J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann
  Automated Termination Proofs for Haskell by Term Rewriting
  ACM Transactions on Programming Languages and Systems, 33(2):7, 2011. © ACM, (2011). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOPLAS, 33(2):7, 2011, http://doi.acm.org/10.1145/1890028.1890030.

• P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
  Automated Termination Proofs for Logic Programs by Term Rewriting
  ACM Transactions on Computational Logic 11(1):1-52, 2009.

• R. Thiemann, H. Zantema, J. Giesl, and P. Schneider-Kamp
  Adding Constants to String Rewriting
  Applicable Algebra in Engineering, Communication and Computing 19(1):27-38, 2008. © Springer-Verlag
  Preliminary version (The final publication is available at www.springerlink.com)

• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Mechanizing and Improving Dependency Pairs
  Journal of Automated Reasoning, 37(3):155-203, 2006. © Springer-Verlag
  Preliminary version (The original publication is available at www.springerlink.com)

• R. Thiemann and J. Giesl
  The Size-Change Principle and Dependency Pairs for Termination of Term Rewriting
  Applicable Algebra in Engineering, Communication and Computing 16(4):229-270, 2005. © Springer-Verlag
  Preliminary version (The original publication is available at www.springerlink.com)

Conferences

52. M. W. Haslbeck and R. Thiemann
    An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR
    In Proceedings of the 10th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '21), pages 238 - 249, 2021.

51. R. Bottesch, M. W. Haslbeck, A. Reynaud and R. Thiemann
    Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL
    In Proceedings of the 12th International NASA Formal Methods Symposium (NFM '20), Lecture Notes in Computer Science 12229, pages 233 - 250, 2020.

50. R. Thiemann, J. Schöpf, C. Sternagel, and A. Yamada
    Certifying the Weighted Path Order
    In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD '20), Leibniz International Proceedings in Informatics 167, pages 4:1 - 4:20, 2020.

49. R. Bottesch, M. W. Haslbeck, and R. Thiemann.
    Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
    In Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS '19), Lecture Notes in Computer Science 11715, pages 223 – 239, 2019.

48. R. Bottesch, M. W. Haslbeck, and R. Thiemann.
    A Verified Efficient Implementation of the LLL Basis Reduction Algorithm
    In Proceedings of the 22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR '18), EPiC Series in Computing 57, pages 164 – 180, 2018.

47. J. Divasón, S. Joosten, R. Thiemann, and A. Yamada.
    A Formalization of the LLL Basis Reduction Algorithm
    In Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP '18), Lecture Notes in Computer Science 10895, pages 160-177, 2018.

46. J. Divasón, S. Joosten, O. Kunčar, R. Thiemann, and A. Yamada.
    Efficient Certification of Complexity Proofs – Formalizing the Perron-Frobenius Theorem
    In Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '18), pages 2-13, 2018.

45. 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, and D. Traytel.
    Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
    In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17), Lecture Notes in Computer Science 10483, pages 3-21, 2017.

44. 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.

43. 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.

42. 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.

41. 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.

40. 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.

39. 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.

38. 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.

37. 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.

36. 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.

35. 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.

34. 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.

33. 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.

32. 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.

31. 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.

30. 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.

29. 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.

28. 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.

27. 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.

26. 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.

25. 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.

24. 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.

22. 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.

21. 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.

20. 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.

19. 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.

18. 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

17. 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.

16. 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

15. 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.

14. 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.

13. 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

12. 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

11. 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

10. 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

9. 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

8. 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

7. 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

6. 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

5. 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

4. 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

3. 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

2. 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.

1. 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

• My PGP key