Lehr- und Forschungsgebiet Informatik 2

Department of Computer Science

René Thiemann

Lehr- und Forschungsgebiet Informatik 2 RWTH Aachen D-52056 Aachen Germany E-Mail: thiemann@informatik.rwth-aachen.de Phone: +49-241/80-21241 Fax: +49-241/80-22217 Room: 4209, Ahornstr. 55

Research

I am a research assistent and PhD student at Lehr- und Forschungsgebiet Informatik 2. My fields of interest include but are not limited to:

• Termination analysis (AProVE tool)
• Term rewriting
• SAT encoding

Teaching Activities (Lehr- und Forschungsgebiet Informatik 2)

• Vorlesung Datenstrukturen und Algorithmen (SS 07)
• Seminar Verifikationsverfahren (SS 07)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 07)
• Vorlesung Termersetzungssysteme (WS 06/07)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (WS 06/07)
• Vorlesung Logikprogrammierung (SS 06)
• Seminar Verifikationsverfahren (SS 06)
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (SS 06)
• Vorlesung 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)
• Vorlesung Termersetzungssysteme (SS 04)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 04)
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (SS 04)
• Vorlesung 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)
• Vorlesung Grundlagen der Funktionalen Programmierung (WS 02/03)
• Seminar Verifikationsverfahren (WS 02/03)
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (SS 02)

Publications

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.

Journals

• R. Thiemann, H. Zantema, J. Giesl, and P. Schneider-Kamp
  Adding Constants to String Rewriting
  Applicable Algebra in Engineering, Communication and Computing, to appear.
• 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

• 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, to appear.
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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.
• 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

René Thiemann

Last modified: Fri Oct 19 11:50:46 CEST 2007