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:

Invited Speaker of the POPL 2013 TutorialFest at the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '13), Rome, Italy, 2013

Invited Speaker of the 6. Arbeitstagung Programmiersprachen at the Multikonferenz Software Engineering (SE '13), Aachen, Germany, 2013

PC-Member of the 24th International Conference on Automated Deduction (CADE '13), Lake Placid, NY, USA, 2013

PC-Member of the 5th International Symposium on Symbolic Computation in Software Science (SCSS '13), Hagenberg, Austria, 2013

PC-Member of the 7th International Conference on Language and Automata Theory and Applications (LATA '13), Bilbao, Spain, 2013

PC-Member of the 8th Workshop on Bytecode Semantics, Verification, Analysis, and Transformation (BYTECODE '13), Rome, Italy, 2013

PC-Member of the 11th International Workshop on Reduction Strategies in Rewriting and Programming (WRS '13), Eindhoven, The Netherlands, 2013

PC-Member of the International Workshop on Haskell and Rewriting Techniques (HART '13), Eindhoven, The Netherlands, 2013

PC-Member of the 13th International Workshop on Termination (WST '13), Bertinoro, Italy, 2013

Member of the Organizing Committee of the 7th Federated Conference on Rewriting, Deduction, and Programming (RDP '13), Eindhoven, The Netherlands, 2013

Member of the organization committee of the Deduktionstreffen 2013, Koblenz, Germany, 2013

Member of the Scientific Advisory Board of the Max-Planck-Institut Informatik, Saarbrücken, Germany

Chair of the IFIP Working Group 1.6 on Term Rewriting

Member of the Steering Committee of the Annual International Termination Competition

Teaching:

Research Topics:

Program Analysis, Verification, Rewriting, Automated Deduction

Selected Publications:

L. Noschinski, F. Emmes, and J. Giesl
Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs
Journal of Automated Reasoning, 51(1):27-56, 2013. ©Springer-Verlag.
Preliminary Version

J. Giesl
Automated Termination Analysis: From Term Rewriting to Programming Languages
In Software Engineering 2013, Workshopband, Proc. 6. Arbeitstagung Programmiersprachen (ATPS 2013), Aachen, Germany, Lecture Notes in Informatics 215, 2013. To appear.

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 7358, pages 105-122, 2012. ©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 7364, pages 225-240, 2012. ©Springer-Verlag

J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs
Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
In Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12), Leuven, Belgium, pages 1-12, 2012. ©ACM Press.
Short version (abstract) appeared in Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '12), Leuven, Belgium, page 1, 2013. ©Springer-Verlag
Extended version appeared as Technical Report AIB-2012-12, RWTH Aachen, Germany.
Slides of a related talk.

M. Codish, Y. Fekete, C. Fuhs, J. Giesl, and J. Waldmann
Exotic Semiring Constraints (Extended Abstract)
In Proceedings of the 10th International Workshop on Satisfiability Modulo Theories (SMT '12), Manchester, UK, pages 87-96, 2012.

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 7421, pages 123-141, 2012. ©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 7225, pages 237-252, 2012. ©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:

Invited Speaker of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12) and the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '12), Leuven, Belgium
Invited Speaker of the Summer School 2012 on Verification Technology, Systems & Applications (VTSA '12), Saarbrücken, Germany
PC-Member of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), Manchester, UK, 2012
Member of the Steering Committee of the ACM/IEEE Symposium on Logic in Computer Science (LICS), 2006 - 2012
Member of the Steering Committee of the Federated Logic Conference (FLoC), 2006 - 2012
Member of the Steering Committee of the International School on Rewriting (ISR), 2006 - 2012
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