Research

I am a research assistent at the Computational Logic group. Previously, I worked as a PhD student under supervision of Jürgen Giesl at the Research Group Computer Science 2, RWTH Aachen University.

My fields of interest include but are not limited to:

• Formalizations of proofs (IsaFoR / CeTA, certification problem format, and Isabelle)
• Termination analysis (tools AProVE and TTT2, and termination competition)
• Term rewriting
• SAT encodings

Upcoming events

• WST 2012, February 19 to 24, 2012, Obergurgl, Austria.
• RTA 2012, May 28 to June 2, 2012, Nagoya, Japan.
• IJCAR 2012, June 25 to 29, 2012, Manchester, UK.
• ITP 2012, August 13 to 16, 2012, Princeton, New Jersey, US. Abstract: February 6, 2012

Teaching Activities

• Lecture Introduction to Model Checking (WS 11/12)
• Lecture Algorithms and Data Structures (SS 11)
• Lecture Model Checking (SS 11)
• Lecture Introduction to Model Checking (WS 10/11)
• Lecture Logic (WS 10/11)
• Specialisation Seminar 99 Bottles of Beer (WS 10/11)
• Lecture and Proseminar Algorithms and Data Structures (SS 10)
• Lecture Model Checking (SS 10)
• Lecture Introduction to Model Checking (WS 09/10)
• Proseminar Logic (WS 09/10)
• Lecture Model Checking (SS 09)
• Proseminar Formal Languages and Automata Theory (SS 09)
• Lecture Introduction to Model Checking (WS 08/09)
• Lecture Introduction to Programming (WS 08/09)
• Proseminar Logic (WS 08/09)
• Lecture Model Checking (SS 08)
• Proseminar Formal Languages and Automata Theory (SS 08)
• Lecture Introduction to Model Checking (WS 07/08)
• Proseminar Logic (WS 07/08)
• Specialisation Seminar Constraint Programming (WS 07/08)
• Lecture (support) Datenstrukturen und Algorithmen (SS 07)
• Seminar Verifikationsverfahren (SS 07)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 07)
• Lecture (support) Termersetzungssysteme (WS 06/07)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (WS 06/07)
• Lecture (support) Logikprogrammierung (SS 06)
• Seminar Verifikationsverfahren (SS 06)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 06)
• Lecture (support) Informatik I - Programmierung (WS 05/06)
• Seminar Automatische Terminierungsanalyse (WS 05/06)
• Seminar Verifikationsverfahren (SS 05)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 05)
• Lecture (support) Termersetzungssysteme (SS 04)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 04)
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (SS 04)
• Lecture (support) Informatik I - Programmierung (WS 03/04)
• Seminar Terminierungsanalyse (WS 03/04)
• Seminar Verifikation von Programmen (SS 03)
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (SS 03)
• Lecture (support) Grundlagen der Funktionalen Programmierung (WS 02/03)
• Seminar Verifikationsverfahren (WS 02/03)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 02)

Publications

PhD Thesis

• R. Thiemann
  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

• 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, to appear. © 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 and Refereed Workshops

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