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://verify.rwth-aachen.de/giesl

Current activities:

Teaching:

• Vorlesung Funktionale Programmierung (Functional Programming), SS 12
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 12
• Seminar Satisfiability Checking, SS 12
• Vorlesung Programmierung (Programming Concepts), WS 11/12
• Seminar Automatische Terminierungsanalyse (Automated Termination Analysis), WS 11/12
• Seminar Satisfiability Checking, WS 11/12
• Vorlesung Termersetzungssysteme (Term Rewriting Systems), SS 11
• Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting), SS 11
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 11
• Vorlesung Logikprogrammierung (Logic Programming), WS 10/11
• Seminar Verifikationsverfahren (Verification Techniques), WS 10/11
• Seminar Satisfiability Checking, WS 10/11
• Vorlesung Formale Systeme, Automaten, Prozesse (Formal Systems, Automata, Processes), SS 10
• Seminar Automatische Terminierungsanalyse (Automated Termination Analysis), SS 10
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 10
• Vorlesung Funktionale Programmierung (Functional Programming), WS 09/10
• Seminar Verifikationsverfahren (Verification Techniques), WS 09/10
• Seminar Satisfiability Checking, WS 09/10
• Vorlesung Programmierung (Programming Concepts), WS 08/09
• Seminar Automatische Terminierungsanalyse (Automated Termination Analysis), WS 08/09
• Vorlesung Logikprogrammierung (Logic Programming), SS 08
• Seminar Verifikationsverfahren (Verification Techniques), SS 08
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 08
• Vorlesung Informatik I - Programmierung (Computer Science I - Programming Concepts), WS 07/08
• Seminar Automatische Terminierungsanalyse (Automated Termination Analysis), WS 07/08
• Vorlesung Grundlagen der Funktionalen Programmierung (Functional Programming), SS 07
• Seminar Verifikationsverfahren (Verification Techniques), SS 07
• Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 07
• 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. Brockschmidt, R. Musiol, C. Otto, and J. Giesl
  Automated Termination Proofs for Java Programs with Cyclic Data
  In Proceedings of the 24th International Conference on Computer Aided Verification (CAV '12), Berkeley, CA, USA, Lecture Notes in Computer Science. To appear. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2012-06, RWTH Aachen, Germany.
• F. Emmes, T. Enger, and J. Giesl
  Proving Non-Looping Non-Termination Automatically
  In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), Manchester, UK, Lecture Notes in Artificial Intelligence. To appear. ©Springer-Verlag
  
• M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
  Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  In Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in Computer Science. To appear. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-19, RWTH Aachen, Germany.
• T. Ströder, F. Emmes, P. Schneider-Kamp, J. Giesl, and C. Fuhs
  A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
  In Proceedings of the 21st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '11), Odense, Denmark, Lecture Notes in Computer Science. To appear. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-08, RWTH Aachen, Germany.
• 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
• J. Giesl and R. Hähnle (eds.)
  Special Issue on the 5th International Joint Conference on Automated Reasoning (IJCAR 2010)
  Journal of Automated Reasoning, 47(4), 2011. ©Springer-Verlag
• C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, and S. Swiderski
  Proving Termination by Dependency Pairs and Inductive Theorem Proving
  Journal of Automated Reasoning, 47(2):133-160, 2011. ©Springer-Verlag
• L. Noschinski, F. Emmes, and J. Giesl
  A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
  In Proceedings of the 23rd International Conference on Automated Deduction (CADE '11), Wroclaw, Poland, Lecture Notes in Artificial Intelligence 6803, pages 422-438, 2011. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-03, RWTH Aachen, Germany.
  Slides of a related talk.
• 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), Nijmegen, The Netherlands, Lecture Notes in Computer Science 6898, pages 152-167, 2011. ©Springer-Verlag
  
• M. Codish, I. Gonopolskiy, A. Ben-Amram, C. Fuhs, and J. Giesl
  SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers
  In Proceedings of the 27th International Conference on Logic Programming (ICLP '11), Lexington, KY, USA, Theory and Practice of Logic Programming, 11(4-5):503-520, 2011. ©Cambridge University Press.
• M. Brockschmidt, C. Otto, and J. Giesl
  Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
  In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia, LIPIcs Leibniz International Proceedings in Informatics 10, pages 155-170, 2011. Dagstuhl Publishing
  Extended version appeared as Technical Report AIB-2011-02, RWTH Aachen, Germany.
  Slides of a related talk.
• 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), 2011.
• M. T. Nguyen, D. De Schreye, J. Giesl, and P. Schneider-Kamp
  Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs
  Theory and Practice of Logic Programming, 11(1):33-63, 2011. ©Cambridge University Press.
• J. Giesl
  Automated Termination Analyzer for Haskell
  Haskell Communities and Activities Report, 21:60, 2011.
• T. Ströder, P. Schneider-Kamp, and J. Giesl
  Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
  In Proceedings of the 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '10), Hagenberg, Austria, Lecture Notes in Computer Science 6564, pages 184-199, 2011. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2010-12, RWTH Aachen, Germany.
• 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 (IWS '10), Edinburgh, UK, EPTCS 44, pages 51-65, 2010.
• M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp
  Lazy Abstraction for Size-Change Termination
  In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), Yogyakarta, Indonesia, Lecture Notes in Computer Science (ARCoSS) 6397, pages 217-232, 2010. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2010-14, RWTH Aachen, Germany.
• M. Brockschmidt, C. Otto, C. von Essen, and J. Giesl
  Termination Graphs for Java Bytecode
  In Verification, Induction, Termination Analysis, Lecture Notes in Artificial Intelligence 6463, pages 17-37, 2010. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2010-15, RWTH Aachen, Germany.
• J. Giesl and R. Hähnle (eds.)
  Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010)
  Edinburgh, UK, Lecture Notes in Artificial Intelligence 6173, 534 pages, Springer-Verlag, 2010.
• C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
  Automated Termination Analysis of Java Bytecode by Term Rewriting
  In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010. Dagstuhl Publishing
  Extended version appeared as Technical Report AIB-2010-08, RWTH Aachen, Germany.
  Slides of a related talk.
• 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), Edinburgh, UK, 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.
  
• J. Giesl
  Current Trends in Automated Deduction
  KI - Künstliche Intelligenz, 24(1):11-13, 2010. Springer-Verlag.
• J. Giesl (ed.)
  Special Issue on Automated Deduction
  KI - Künstliche Intelligenz, 24(1), 2010. Springer-Verlag.
• P. Schneider-Kamp, J. Giesl, and M. T. Nguyen
  The Dependency Triple Framework for Termination of Logic Programs
  In Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '09), Coimbra, Portugal, Lecture Notes in Computer Science 6037, pages 37-51, 2010. ©Springer-Verlag
  
• S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. Schneider-Kamp
  Termination Analysis by Dependency Pairs and Inductive Theorem Proving
  In Proceedings of the 22nd International Conference on Automated Deduction (CADE '09), Montreal, Canada, Lecture Notes in Artificial Intelligence 5663, pages 322-338, 2009. ©Springer-Verlag
  
• C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke
  Proving Termination of Integer Term Rewriting
  In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasilia, Brazil, Lecture Notes in Computer Science 5595, pages 32-47, 2009. ©Springer-Verlag
  
• 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), 2009.
  Preliminary Version
  
• B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, 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 Artificial Intelligence 5330, pages 636-651, 2008. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2008-13, RWTH Aachen, Germany.
  
• 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 appeared as Technical Report AIB-2008-03, RWTH Aachen, Germany.
  
• 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
  
• C. Fuhs, R. Navarro-Marset, C. Otto, J. Giesl, S. Lucas, and P. Schneider-Kamp
  Search Techniques for Rational Polynomial Orders
  In Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC '08), Birmingham, UK, Lecture Notes in Computer Science 5144, pages 109-124, 2008. ©Springer-Verlag
  
• J. Giesl (ed.)
  Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007)
  Paris, France, Electronic Notes in Theoretical Computer Science, Volume 204, 198 pages, Elsevier, 2008.
• M. T. Nguyen, J. Giesl, P. Schneider-Kamp, and D. De Schreye
  Termination Analysis of Logic Programs based on Dependency Graphs
  In Proceedings of the 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '07), Kongens Lyngby, Denmark, Lecture Notes in Computer Science 4915, pages 8-22, 2008. ©Springer-Verlag
  
• 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
  
• 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 International Conference on Automated Deduction (CADE '07), Bremen, Germany, Lecture Note in Artificial Intelligence 4603, pages 443-459, 2007. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2007-03, RWTH Aachen, Germany.
  
• 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
  
• J. Giesl, A. Kühnemann, and J. Voigtländer
  Deaccumulation Techniques for Improving Provability
  Journal of Logic and Algebraic Programming, 71:79-113, 2007. Elsevier.
  Preliminary Version
• 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, 2007. ©Springer-Verlag
  
• J. Giesl (ed.)
  Special Issue on the 16th International Conference on Rewriting Techniques and Applications (RTA 2005)
  Information and Computation 205(4), 2007. Elsevier.
• 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
• J. Giesl and D. Kapur (eds.)
  Third Special Issue on "Techniques for Automated Termination Proofs"
  Journal of Automated Reasoning 37(3), 2006.
• 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, 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, 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 and D. Kapur (eds.)
  Second Special Issue on "Techniques for Automated Termination Proofs"
  Journal of Automated Reasoning 34(4), 2005.
• 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 167-182, 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.

Previous activities:

• PC-Member of the 23rd International Conference on Automated Deduction (CADE '11), Wroclaw, Poland, 2011
• PC-Member of the 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '11), Novi Sad, Serbia, 2011
• PC-Member of the 22nd International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia, 2011
• PC-Member of the 8th International Symposium Frontiers of Combining Systems (FroCoS '11), Saarbrücken, Germany, 2011
• Member of the organization committee of the Deduktionstreffen 2011, Karlsruhe, Germany, 2011
• Member of the Board of Trustees of the International Conference on Automated Deduction (CADE), 2010 - 2011
• Program Co-Chair of the 5th International Joint Conference on Automated Reasoning (IJCAR '10), Edinburgh, Scotland, UK, 2010
• PC-Member of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10), Dakar, Senegal, 2010
• Member of the organization committee of the Deduktionstreffen 2010, Karlsruhe, Germany, 2010
• PC-Member of the 22nd International Conference on Automated Deduction (CADE '09), Montreal, Canada, 2009
• PC-Member of the 20th International Conference on Rewriting Techniques and Applications (RTA '09), Brasilia, Brazil, 2009
• PC-Member of the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '09), Brasilia, Brazil, 2009
• PC-Member of the 32nd Annual Conference on Artificial Intelligence (KI '09), Paderborn, Germany, 2009
• Co-Organizer of the Dagstuhl Seminar Interaction versus Automation: The two Faces of Deduction, Dagstuhl, Germany, 2009
• Member of the organization committee of the Deduktionstreffen 2009, Bremen, Germany, 2009
• PC-Member of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, 2008
• PC-Member of the 4th International Joint Conference on Automated Reasoning (IJCAR '08), Sydney, Australia, 2008
• PC-Member of the 19th International Conference on Rewriting Techniques and Applications (RTA '08), Hagenberg, Austria, 2008
• PC-Member of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS '08), Budapest, Hungary, 2008
• PC-Member of the 7th International Workshop on Rewriting Logic and its Applications (WRLA '08), Budapest, Hungary, 2008
• Co-Organizer of the Dagstuhl Seminar Deduction and Decision Procedures, Dagstuhl, Germany, 2007
• Chair of the Steering Committee of the International Conference on Rewriting Techniques and Applications (RTA) (2005 - 2007), Member of the SC from 2004 - 2007
• Lecturer at the International School on Rewriting (ISR) 2006 & 2007
• PC-Member of the 18th International Conference on Rewriting Techniques and Applications (RTA '07), Paris, France
• Program Chair of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '07), Paris, France
• PC-Member of the 9th International Workshop on Termination (WST '07), Paris, France
• Member of the organization committee of the Deduktionstreffen 2007, Koblenz, Germany, 2007
• Editor of a special issue of the journal Information and Computation devoted to the 16th International Conference 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
• 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, 2006
• PC-Member of the 6th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '06), Seattle, USA
• 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