Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

Prof. Dr. Jürgen Giesl

Address: Lehr- und Forschungsgebiet Informatik 2 Fachgruppe Informatik RWTH Aachen Ahornstr. 55 52074 Aachen Germany Office: Room 4212, 2nd floor, Building E1 (Erweiterungsbau 1), Ahornstr. 55 Phone: +49 241 80-21230 Fax: +49 241 80-22217 Email: Web: http://www-i2.informatik.rwth-aachen.de/giesl

Current activities:

• Invited Speaker of the 17th International Conference on Rewriting Techniques and Applications (RTA '06), Seattle, USA
• PC-Member of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-13), Phnom Penh, Cambodia
• PC-Member of the 6th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '06), Seattle, USA
• Editor of a special issue of the journal Information and Computation devoted to the 16th International Conference on Workshop on Rewriting Techniques and Applications (RTA '05)
• Co-editor of three special issues of the Journal of Automated Reasoning on Techniques for Automated Termination Proofs
• Chair of the Steering Committee of the International Conference on Rewriting Techniques and Applications (RTA)
• Vice-Chair of the IFIP Working Group 1.6 on Term Rewriting

Teaching:

• Vorlesung Termersetzungssysteme (Term Rewriting Systems), WS 06/07
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting), WS 06/07
• Vorlesung Logikprogrammierung (Logic Programming), SS 06
• Seminar Verifikationsverfahren (Verification Techniques), SS 06
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 06
• Vorlesung Informatik I - Programmierung (Computer Science I - Programming Concepts), WS 05/06
• Seminar Automatische Terminierungsanalyse (Automated Termination Analysis), WS 05/06
• Vorlesung Grundlagen der Funktionalen Programmierung (Functional Programming), SS 05
• Seminar Verifikationsverfahren (Verification Techniques), SS 05
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 05
• Vorlesung Termersetzungssysteme (Term Rewriting Systems), SS 04
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting), SS 04
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (IT-Security Concepts and Security in Java), SS 04
• Vorlesung Informatik I - Programmierung (Computer Science I - Programming Concepts), WS 03/04
• Seminar Terminierungsanalyse (Termination Analysis), WS 03/04
• Vorlesung Automatisierte Programmverifikation (Mechanized Program Verification), SS 03
• Seminar Verifikation von Programmen (Program Verification), SS 03
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (IT-Security Concepts and Security in Java), SS 03
• Vorlesung Grundlagen der Funktionalen Programmierung (Functional Programming), WS 02/03
• Seminar Verifikationsverfahren (Verification Techniques), WS 02/03
• Vorlesung Termersetzungssysteme (Term Rewriting Systems), SS 02
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting), SS 02
• Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (IT-Security Concepts and Security in Java), SS 02
• Vorlesung Informatik I - Programmierung (Computer Science I - Programming Concepts), WS 01/02
• Seminar Verifikation von Programmen (Program Verification), WS 01/02
• Vorlesung Grundlagen der Funktionalen Programmierung (Functional Programming), SS 01
• Seminar Push-Button Verifikation (Push-Button Verification), SS 01
• Vorlesung Automatisierte Programmverifikation (Mechanized Program Verification), WS 00/01
• Seminar Verifikationswerkzeuge und -verfahren (Verification Tools and Techniques), WS 00/01

Research Topics:

Selected Publications:

• 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, 2006. To appear.©Springer-Verlag
  
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation Techniques for Improving Provability
  Journal of Logic and Algebraic Programming, 2006. To appear.
  
• 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, 2006. To appear.©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, 2006. To appear.©Springer-Verlag
  
• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Mechanizing and Improving Dependency Pairs
  Journal of Automated Reasoning, 2006. To appear.
  
• 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, 2006. To appear.©Springer-Verlag
  
• J. Giesl and D. Kapur (eds.)
  Special Issue on "Techniques for Automated Termination Proofs"
  Journal of Automated Reasoning 34(2), 2005.
• J. Giesl, R. Thiemann, 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
  Extended version appeared as Technical Report AIB-2005-03, RWTH Aachen, Germany.
  
• 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
  
• J. Giesl (ed.)
  Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005)
  Nara, Japan, Lecture Notes in Computer Science 3467, 517 pages, Springer-Verlag, 2005.
  
• J. Giesl, R. Thiemann, 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 2004), Montevideo, Uruguay, Lecture Notes in Artificial Intelligence 3452, pages 301-331, 2005. ©Springer-Verlag
  
• R. Thiemann, J. Giesl, P. Schneider-Kamp
  Improved Modular Termination Proofs Using Dependency Pairs
  In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR 2004), 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 and A. Middeldorp
  Transformation Techniques for Context-Sensitive Rewrite Systems
  Journal of Functional Programming, 14(4): 379-427, 2004.
  Extended Version appeared as Technical Report AIB-2002-02, RWTH Aachen, Germany.
• D. Kapur, J. Giesl, and M. Subramaniam
  Induction and Decision Procedures
  Revista de la real academia de ciencas (RACSAM), Serie A: Matematicas, 98(1): 153-180, 2004.
• J. Giesl
  Terese, Term Rewriting Systems (Review)
  Bulletin of Symbolic Logic, 10(2): 223-225, 2004.
• 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 165-179, 2003. ©Springer-Verlag
  Extended version available as Technical Report AIB-2003-04, RWTH Aachen, Germany.
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation - Improving Provability
  In Proceedings of the 8th Asian Computing Science Conference (ASIAN '03), Mumbai, India, Lecture Notes in Computer Science 2896, pages 146-160, 2003. ©Springer-Verlag
• J. Giesl and H. Zantema
  Simulating Liveness by Reduction Strategies
  In Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS '03), Valencia, Spain, Electronic Notes in Theoretical Computer Science 86 (4), 2003. ©Elsevier
• J. Giesl and D. Kapur
  Deciding Inductive Validity of Equations
  In Proceedings of the 19th International Conference on Automated Deduction (CADE-19), Miami, FL, USA, Lecture Notes in Artificial Intelligence 2741, pages 17-31, 2003. ©Springer-Verlag
  Extended version available as Technical Report AIB-2003-03, 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.
• J. Giesl and H. Zantema
  Liveness in Rewriting
  In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA-03), Valencia, Spain, Lecture Notes in Computer Science 2706, pages 321-336, 2003. ©Springer-Verlag
  Extended versions available as Technical Report AIB-2002-11, RWTH Aachen, Germany and as CS-Report 01-03, Technical University Eindhoven, The Netherlands.
• J. Giesl and A. Middeldorp
  Innermost Termination of Context-Sensitive Rewriting
  In Proceedings of the 6th International Conference on Developments in Language Theory (DLT 2002), Kyoto, Japan, Lecture Notes in Computer Science 2450, pages 231-244, 2003. ©Springer-Verlag
  Extended version available as Technical Report AIB-2002-04, RWTH Aachen, Germany.
• J. Giesl, T. Arts, and E. Ohlebusch
  Modular Termination Proofs for Rewriting Using Dependency Pairs
  Journal of Symbolic Computation 34(1):21-58, 2002.
  Preliminary Version
• J. Giesl and T. Arts
  Verification of Erlang Processes by Dependency Pairs
  Applicable Algebra in Engineering, Communication and Computing 12(1,2):39-72, 2001.
  The original publication is available on LINK at http://link.springer.de © Springer-Verlag
  Preliminary Version
• J. Giesl and P. Lescanne (eds.)
  Special Issue on "Termination"
  Applicable Algebra in Engineering, Communication and Computing 12(1,2), 2001.
  The special issue is available on LINK at http://link.springer.de © Springer-Verlag
• J. Giesl and D. Kapur
  Decidable Classes of Inductive Theorems
  In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001), Siena, Italy, Lecture Notes in Artificial Intelligence 2083, pages 469-484, 2001. ©Springer-Verlag
• J. Giesl and D. Kapur
  Dependency Pairs for Equational Rewriting
  In Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA-01), Utrecht, The Netherlands, Lecture Notes in Computer Science 2051, pages 93-107, 2001. ©Springer-Verlag
  Extended version available as Technical Report TR-CS-2000-53, University of New Mexico, USA.
• J. Giesl
  Induction Proofs with Partial Functions
  Journal of Automated Reasoning 26(1):1-49, 2001.
  Preliminary version appeared as Technical Report IBN 98/48, TU Darmstadt, Germany.
• T. Arts and J. Giesl
  A Collection of Examples for Termination of Term Rewriting Using Dependency Pairs
  Technical Report AIB-2001-09, RWTH Aachen, Germany.
• J. Giesl
  Context-Moving Transformations for Function Verification
  In Proceedings of the 9th International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR '99), Venice, Italy, Lecture Notes in Computer Science 1817, pages 293-312, 2000. ©Springer-Verlag
  Extended version available as Technical Report IBN 99/51, Darmstadt University of Technology, Germany.
• D. Duffy and J. Giesl
  Closure Induction in a Z-like Language
  In Proceedings of the International Conference of Z and B Users (ZB2000), York, UK, Lecture Notes in Computer Science 1878, pages 471-490, 2000. ©Springer-Verlag
• H. Ohsaki, A. Middeldorp, and J. Giesl
  Equational Termination by Semantic Labelling
  In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL '00), Fischbachau/Munich, Germany, Lecture Notes in Computer Science 1862, pages 457-471, 2000. ©Springer-Verlag
• J. Giesl and A. Middeldorp
  Eliminating Dummy Elimination
  In Proceedings of the 17th International Conference on Automated Deduction (CADE-17), Pittsburgh, PA, USA, Lecture Notes in Artificial Intelligence 1831, pages 309-323, 2000. ©Springer-Verlag
• T. Arts and J. Giesl
  Termination of Term Rewriting Using Dependency Pairs
  Theoretical Computer Science 236:133-178, 2000.
  Preliminary Version
  Extended preliminary version (including a large collection of examples) appeared as Technical Report IBN 97/46, TU Darmstadt, Germany.
• J. Giesl and E. Ohlebusch
  Pushing the Frontiers of Combining Rewrite Systems Farther Outwards
  In Proceedings of the Second International Workshop on Frontiers of Combining Systems (FroCoS '98), Amsterdam, The Netherlands, Studies in Logic and Computation 7, pages 141-160, Research Studies Press, John Wiley & Sons, 2000.
• J. Brauburger and J. Giesl
  Approximating the Domains of Functional and Imperative Programs
  Science of Computer Programming 35:113-136, 1999.
  Preliminary Version
• T. Arts and J. Giesl
  Applying Rewriting Techniques to the Verification of Erlang Processes
  In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL '99), Madrid, Spain, Lecture Notes in Computer Science 1683, pages 96-110, 1999. ©Springer-Verlag
• J. Giesl and A. Middeldorp
  Transforming Context-Sensitive Rewrite Systems
  In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), Trento, Italy, Lecture Notes in Computer Science 1631, pages 271-285, 1999. ©Springer-Verlag
• J. Giesl
  The Critical Pair Lemma: A Case Study for Induction Proofs with Partial Functions
  Technical Report IBN 98/49, Darmstadt University of Technology, Germany, 1998.
• J. Giesl
  Partial Functions in Induction Theorem Proving
  In Proceedings of the Workshop on the Mechanization of Partial Functions, held in conjunction with the 15th International Conference on Automated Deduction, Lindau, Germany, 1998.
• J. Brauburger and J. Giesl
  Termination Analysis by Inductive Evaluation
  In Proceedings of the 15th International Conference on Automated Deduction (CADE-15), Lindau, Germany, Lecture Notes in Artificial Intelligence 1421, pages 254-269, 1998. ©Springer-Verlag
  Extended version appeared as Technical Report IBN 98/47, TU Darmstadt.
• J. Giesl, C. Walther, and J. Brauburger
  Termination Analysis for Functional Programs
  In Automated Deduction - A Basis for Applications, Vol. 3 (Applications), W. Bibel and P. Schmitt (eds.), pages 135-164, Applied Logic Series 10, Kluwer Academic Publishers, 1998.
  Preliminary Version
• T. Arts and J. Giesl
  Modularity of Termination Using Dependency Pairs
  In Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), Tsukuba, Japan, Lecture Notes in Computer Science 1379, pages 226-240, Springer-Verlag, 1998.
  Extended version available as Technical Report IBN 97/45, Darmstadt University of Technology, Germany.
• J. Giesl
  Termination of Nested and Mutually Recursive Algorithms
  Journal of Automated Reasoning 19:1-29, 1997.
  Preliminary version appeared as Technical Report IBN 96/30, TU Darmstadt, Germany.
• T. Arts and J. Giesl
  Proving Innermost Normalisation Automatically
  In Proceedings of the 8th International Conference on Rewriting Techniques and Applications (RTA-97), Sitges, Spain, Lecture Notes in Computer Science 1232, pages 157-171, Springer-Verlag, 1997.
  Extended version available as Technical Report IBN 96/39, Technische Hochschule Darmstadt, Germany.
• T. Arts and J. Giesl
  Automatically Proving Termination Where Simplification Orderings Fail
  In Proceedings of the 7th International Joint Conference on the Theory and Practice of Software Development (TAPSOFT'97), Lille, France, Lecture Notes in Computer Science 1214, pages 261-272, Springer-Verlag, 1997.
  Extended version available as Technical Report UU-CS-1996-44, Utrecht University, The Netherlands.
• J. Brauburger and J. Giesl
  Termination Analysis for Partial Functions
  In Proceedings of the Third International Static Analysis Symposium (SAS'96), Aachen, Germany, Lecture Notes in Computer Science 1145, pages 113-127, Springer-Verlag, 1996.
  Extended version available as Technical Report IBN 96/33, Technische Hochschule Darmstadt, Germany.
• J. Giesl
  Proving Partial Correctness of Partial Functions
  In Proceedings of the Workshop on the Mechanization of Partial Functions, held in conjunction with the 13th International Conference on Automated Deduction , New Brunswick, NJ, USA, 1996.
• T. Arts and J. Giesl
  Termination of Constructor Systems
  In Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96), New Brunswick, NJ, USA, Lecture Notes in Computer Science 1103, pages 63-77, Springer-Verlag, 1996.
  Extended versions available as Technical Report IBN 96/34, Technische Hochschule Darmstadt, Germany and as Technical Report UU-CS-1996-07, Utrecht University, The Netherlands.
• J. Giesl
  Termination Analysis for Functional Programs using Term Orderings
  In Proceedings of the Second International Static Analysis Symposium (SAS'95), Glasgow, Scotland, Lecture Notes in Computer Science 983, pages 154-171, Springer-Verlag, 1995.
• J. Giesl
  Automated Termination Proofs with Measure Functions
  In Proceedings of the 19th German Annual Conference on Artificial Intelligence (KI-95), Bielefeld, Germany, Lecture Notes in Artificial Intelligence 981, pages 149-160, Springer-Verlag, 1995.
• J. Giesl
  POLO - A System for Termination Proofs using Polynomial Orderings
  Technical Report IBN 95/24, Technische Hochschule Darmstadt, 1995.
• J. Giesl
  Generating Polynomial Orderings for Termination Proofs
  In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), Kaiserslautern, Germany, Lecture Notes in Computer Science 914, pages 426-431, Springer-Verlag, 1995.
  Extended Version available as Technical Report IBN 95/23, Technische Hochschule Darmstadt, Germany.
• J. Giesl
  Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen.
  Dissertation, Infix-Verlag, Sankt Augustin, 1995.
• J. Giesl and I. Neumann
  The Semantics of Rational Contractions
  Technical Report 29/94, Universität Karlsruhe, Germany, 1994.
• J. Giesl and I. Neumann
  Strategies for Semantical Contractions (Abstract)
  In Proceedings of the 18th German Annual Conference on Artificial Intelligence (KI-94), Saarbrücken, Germany, Lecture Notes in Artificial Intelligence 861, Springer-Verlag, 1994.
• J. Giesl and I. Neumann
  The Semantics of Rational Contractions (Abstract)
  In Proceedings of the 6th Portuguese Conference on Artificial Intelligence (EPIA'93), Porto, Portugal, Lecture Notes in Artificial Intelligence 727, Springer-Verlag, 1993.

Recent activities:

• Program Chair of the 16th International Conference on Workshop on Rewriting Techniques and Applications (RTA '05), Nara, Japan
• PC-Member of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05), Vienna, Austria
• PC-Member of the 4th International Workshop on Parallel and Distributed Methods in Verification (PDMC '05), Lisbon, Portugal
• Invited Speaker of the CADE 20 - Workshop on Disproving, Tallinn, Estonia
• Invited Speaker of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR '04), Montevideo, Uruguay
• Conference Chair of the Federated Conference on Rewriting, Deduction, and Programming 2004 (RDP '04), Aachen, Germany
• Conference Chair of the 15th International Conference on Rewriting Techniques and Applications (RTA '04), Aachen, Germany
• PC-member of the 15th International Conference on Rewriting Techniques and Applications (RTA '04), Aachen, Germany
• PC-member of the 4th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '04), Aachen, Germany
• PC-member of the Doctoral Programme at the 2nd International Joint Conference on Automated Reasoning (IJCAR '04), Cork, Ireland
• PC-member of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS '03), Valencia, Spain
• PC-member of the 6th International Workshop on Termination (WST '03), Valencia, Spain
• PC-member of the 13th International Conference on Rewriting Techniques and Applications (RTA '2002), Copenhagen, Denmark
• PC-member of the 5th International Workshop on Termination (WST '01), Utrecht, The Netherlands
• PC-member of the 11th International Conference on Rewriting Techniques and Applications (RTA '2000), Norwich, UK
• PC-member of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR '99), Tblisi, Georgia
• Organizer and PC-chair of the 4th International Workshop on Termination (WST '99), Dagstuhl, Germany
• Co-organizer of the CADE '98 Workshop on the Mechanization of Partial Functions, Lindau, Germany

Last modified: Wed Apr 14 16:30:22 CEST 2004 / Jürgen Giesl