Lehr- und Forschungsgebiet Informatik 2

Fachgruppe Informatik

RWTH

Prof. Dr. Jürgen Giesl

LuFG


			Current Activities PC-Member of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), Nancy, France, 2024 PC Member of the 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '24), Mauritius, 2024 President of the Board of Trustees of the International Conference on Automated Deduction (CADE), since 2022. Member from 2010 - 2011 and 2014 - 2020. Member of the Steering Committee of the International Conference on Formal Structures for Computation and Deduction (FSCD), since 2022 Member of the Steering Committee of the International Joint Conference on Automated Reasoning (IJCAR), since 2022 Member of the Board of the Association for Automated Reasoning Member of the IFIP Working Group 1.6 on Term Rewriting Member of the Steering Committee of the Annual International Termination Competition Member of the Editorial Board of the ACM Transactions on Computational Logic (Area Editor for Automated Reasoning, Term Rewriting, Program Verification) Teaching Vorlesung Programmierung (Programming Concepts), WS 24/25 Seminar Verifikationsverfahren (Verification Techniques), WS 24/25 Vorlesung Foundations of Functional Programming, SS 24 Seminar Satisfiability Checking, SS 24 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 24 Vorlesung Programmierung (Programming Concepts), WS 23/24 Seminar Verifikationsverfahren (Verification Techniques), WS 23/24 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 23 Vorlesung Programmierung (Programming Concepts), WS 22/23 Seminar Verifikationsverfahren (Verification Techniques), WS 22/23 Vorlesung Logikprogrammierung (Logic Programming), SS 22 Seminar Satisfiability Checking, SS 22 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 22 Vorlesung Programmierung (Programming Concepts), WS 21/22 Seminar Verifikationsverfahren (Verification Techniques), WS 21/22 Vorlesung Funktionale Programmierung (Functional Programming), SS 21 Seminar Satisfiability Checking, SS 21 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 21 Vorlesung Programmierung (Programming Concepts), WS 20/21 Seminar Verifikationsverfahren (Verification Techniques), WS 20/21 Vorlesung Logikprogrammierung (Logic Programming), SS 20 Seminar Satisfiability Checking, SS 20 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 20 Vorlesung Programmierung (Programming Concepts), WS 19/20 Seminar Verifikationsverfahren (Verification Techniques), WS 19/20 Vorlesung Funktionale Programmierung (Functional Programming), SS 19 Seminar Verifikationsverfahren (Verification Techniques), SS 19 Seminar Satisfiability Checking, SS 19 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 19 Vorlesung Programmierung (Programming Concepts), WS 18/19 Seminar Verifikationsverfahren (Verification Techniques), WS 18/19 Vorlesung Programmierung (Programming Concepts), WS 17/18 Seminar Verifikationsverfahren (Verification Techniques), WS 17/18 Vorlesung Logikprogrammierung (Logic Programming), SS 17 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 17 Seminar Satisfiability Checking, SS 17 Vorlesung Programmierung (Programming Concepts), WS 16/17 Seminar Verifikationsverfahren (Verification Techniques), WS 16/17 Vorlesung Funktionale Programmierung (Functional Programming), SS 16 Seminar Satisfiability Checking, SS 16 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), SS 16 Vorlesung Termersetzungssysteme (Term Rewriting Systems), WS 15/16 Seminar Termersetzungssysteme - Aktuelle Themen und Erweiterungen (Advanced Topics in Term Rewriting), WS 15/16 Proseminar Fortgeschrittene Programmierkonzepte (Advanced Programming Concepts), WS 15/16 Vorlesung Logikprogrammierung (Logic Programming), SS 15 Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 15 Seminar Satisfiability Checking, SS 15 Vorlesung Programmierung (Programming Concepts), WS 14/15 Seminar Verifikationsverfahren (Verification Techniques), WS 14/15 Vorlesung Funktionale Programmierung (Functional Programming), SS 14 Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 14 Seminar Satisfiability Checking, SS 14 Vorlesung Logikprogrammierung (Logic Programming), SS 13 Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (Advanced Programming Concepts in Java, Haskell, and Prolog), SS 13 Seminar Satisfiability Checking, SS 13 Vorlesung Programmierung (Programming Concepts), WS 12/13 Seminar Verifikationsverfahren (Verification Techniques), WS 12/13 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 Selected Publications F. Frohn and J. Giesl Integrating Loop Acceleration into Bounded Model Checking In Proceedings of the 26th International Symposium on Formal Methods (FM '24), Milano, Italy, Lecture Notes in Computer Science 14933, pages 73-91, 2024. Extended version appeared at arXiv, CoRR abs/2401.09973. F. Baader and J. Giesl On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems In Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD '24), Tallinn, Estonia, LIPIcs 299, pages 16:1-16:18, 2024. F. Frohn and J. Giesl Satisfiability Modulo Exponential Integer Arithmetic In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), Nancy, France, Lecture Notes in Computer Science 14739, pages 344-365, 2024. Extended version appeared at arXiv, CoRR abs/2402.01501. J.-C. Kassing, G. Vartanyan, and J. Giesl A Dependency Pair Framework for Relative Termination of Term Rewriting In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), Nancy, France, Lecture Notes in Computer Science 14740, pages 360-380, 2024. Extended version appeared at arXiv, CoRR abs/2404.15248. N. Lommen, E. Meyer, and J. Giesl Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper) In Proceedings of the 12th International Joint Conference on Automated Reasoning (IJCAR '24), Nancy, France, Lecture Notes in Computer Science 14739, pages 233-243, 2024. Extended version appeared at arXiv, CoRR abs/2402.03891. J.-C. Kassing, S. Dollase, and J. Giesl A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting In Proceedings of the 17th International Symposium on Functional and Logic Programming (FLOPS '24), Kumamoto, Japan, Lecture Notes in Computer Science 14659, pages 62-80, 2024. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2309.00344. J.-C. Kassing, F. Frohn, and J. Giesl From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting In Proceedings of the 27th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '24), Luxembourg City, Luxembourg, Lecture Notes in Computer Science 14575, pages 206-228, 2024. Extended version appeared at arXiv, CoRR abs/2310.06121. AProVE artifact available at Zenodo M. Hark, F. Frohn, and J. Giesl Termination of Triangular Polynomial Loops Formal Methods in System Design, 2023. Preliminary version appeared at arXiv, CoRR abs/1910.11588. Slides of a related talk. F. Frohn and J. Giesl ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses In Proceedings of the 30th Static Analysis Symposium (SAS '23), Cascais, Portugal, Lecture Notes in Computer Science 14284, pages 259-285, 2023. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2303.01827. N. Lommen and J. Giesl Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs In Proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS '23), Prague, Czech Republic, Lecture Notes in Artificial Intelligence 14279, pages 3-22, 2023. Extended version appeared at arXiv, CoRR abs/2307.06921. J.-C. Kassing and J. Giesl Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs In Proceedings of the 29th International Conference on Automated Deduction (CADE '23), Rome, Italy, Lecture Notes in Artificial Intelligence 14132, pages 344-364, 2023. Extended version appeared at arXiv, CoRR abs/2305.11741. J. Hensel and J. Giesl Proving Termination of C Programs with Lists In Proceedings of the 29th International Conference on Automated Deduction (CADE '23), Rome, Italy, Lecture Notes in Artificial Intelligence 14132, pages 266-285, 2023. Extended version appeared at arXiv, CoRR abs/2305.12159. Slides of a related talk. F. Frohn and J. Giesl Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper) In Proceedings of the 29th International Conference on Automated Deduction (CADE '23), Rome, Italy, Lecture Notes in Artificial Intelligence 14132, pages 220-233, 2023. Extended version appeared at arXiv, CoRR abs/2304.10166. N. Lommen, F. Meyer, and J. Giesl Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR '22), Haifa, Israel, Lecture Notes in Artificial Intelligence 13385, pages 734-754, 2022. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2205.08869. F. Frohn and J. Giesl Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) In Proceedings of the 11th International Joint Conference on Automated Reasoning (IJCAR '22), Haifa, Israel, Lecture Notes in Artificial Intelligence 13385, pages 712-722, 2022. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2202.04546. J. Giesl, N. Lommen, M. Hark, and F. Meyer Improving Automatic Complexity Analysis of Integer Programs In The Logic of Software: A Tasting Menu of Formal Methods, Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 13360, pages 193-228, 2022. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2202.01769. J. Hensel, C. Mensendiek, and J. Giesl AProVE: Non-Termination Witnesses for C Programs (Competition Contribution) In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '22), Lecture Notes in Computer Science 13244, pages 403-407, 2022. ⒸSpringer-Verlag F. Meyer, M. Hark, and J. Giesl Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '21), Lecture Notes in Computer Science 12651, pages 250-269, 2021. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/2010.06367. Slides of a related talk. F. Frohn, M. Hark, and J. Giesl Termination of Polynomial Loops In Proceedings of the 27th Static Analysis Symposium (SAS '20), Lecture Notes in Computer Science 12389, pages 89-112, 2021. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/1910.11588. F. Frohn, M. Naaf, M. Brockschmidt, and J. Giesl Inferring Lower Runtime Bounds for Integer Programs ACM Transactions on Programming Languages and Systems, 42(3), 2020. Preliminary version appeared at arXiv, CoRR abs/1911.01077. M. Hark, F. Frohn, and J. Giesl Polynomial Loops: Beyond Termination In Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '20), EPiC Series in Computing 73, pages 279-297, 2020. M. Hark, B. L. Kaminski, J. Giesl, and J.-P. Katoen Aiming Low Is Harder - Induction for Lower Bounds in Probabilistic Program Verification In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '20), New Orleans, LA, USA, Proceedings of the ACM on Programming Languages, 4, Article 37, 2020. Extended version appeared at arXiv, CoRR abs/1904.011117. F. Frohn and J. Giesl Proving Non-Termination via Loop Acceleration In Proceedings of the 19th International Conference on Formal Methods in Computer-Aided Design (FMCAD '19), San Jose, CA, USA, IEEE Press, pages 221-230, 2019. Extended version appeared at arXiv, CoRR abs/1905.11187. J. Giesl, P. Giesl, and M. Hark Computing Expected Runtimes for Constant Probability Programs In Proceedings of the 27th International Conference on Automated Deduction (CADE '19), Natal, Brazil, Lecture Notes in Artificial Intelligence 11716, pages 269-286, 2019. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/1905.09544. Slides of a related talk. F. Frohn and J. Giesl Termination of Triangular Integer Loops is Decidable In Proceedings of the 31st International Conference on Computer Aided Verification (CAV '19), New York, NY, USA, Lecture Notes in Computer Science 11562, pages 426-444, 2019. ⒸSpringer-Verlag Extended version appeared at arXiv, CoRR abs/1905.08664. J. Giesl, A. Rubio, C. Sternagel, J. Waldmann, and A. Yamada The Termination and Complexity Competition In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19), Part III, Prague, Czech Republic, Lecture Notes in Computer Science 11429, pages 156-166, 2019. ⒸSpringer-Verlag F. Frohn and J. Giesl Constant Runtime Complexity of Term Rewriting is Semi-Decidable Information Processing Letters, 139:18-23, 2018. ⒸElsevier Preliminary Version Slides of a related talk. J. Hensel, J. Giesl, F. Frohn, and T. Ströder Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution Journal of Logical and Algebraic Methods in Programming, 97:105-130, 2018. ⒸElsevier Preliminary Version Slides of a related talk. F. Frohn and J. Giesl Complexity Analysis for Java with AProVE In Proceedings of the 13th International Conference on integrated Formal Methods (iFM 2017), Turin, Italy, Lecture Notes in Computer Science 10510, pages 85-101, 2017. Winner of the Best Tool Paper Award of the conference. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2017-04, RWTH Aachen University, Germany. Slides of a related talk. M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl Complexity Analysis for Term Rewriting by Integer Transition Systems In Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017), Brasilia, Brazil, Lecture Notes in Artificial Intelligence 10483, pages 132-150, 2017. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2017-05, RWTH Aachen University, Germany. F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder Lower Bounds for Runtime Complexity of Term Rewriting Journal of Automated Reasoning, 59(1):121-163, 2017. ⒸSpringer-Verlag The final publication is available at Springer via the DOI 10.1007/s10817-016-9397-x. Preliminary Version Slides of a related talk. J. Giesl and J. Hoffmann (eds.) Special Issue on Automatic Resource Bound Analysis Journal of Automated Reasoning, 59(1), 2017. ⒸSpringer-Verlag J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution) In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17), Uppsala, Sweden, Lecture Notes in Computer Science 10206, pages 350-354, 2017. ⒸSpringer-Verlag F. Frohn and J. Giesl Analyzing Runtime Complexity via Innermost Runtime Complexity In Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '17), Maun, Botswana, EPiC Series in Computing 46, pages 249-268, 2017. Extended version appeared as Technical Report AIB-2017-02, RWTH Aachen University, Germany. J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing Program Termination and Complexity Automatically with AProVE Journal of Automated Reasoning, 58(1):3-31, 2017. ⒸSpringer-Verlag The final publication is available at Springer via the DOI 10.1007/s10817-016-9388-y. Preliminary Version T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, P. Schneider-Kamp, and C. Aschermann Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic Journal of Automated Reasoning, 58(1):33-65, 2017. ⒸSpringer-Verlag The final publication is available at Springer via the DOI 10.1007/s10817-016-9389-x. Preliminary Version Extended version appeared as Technical Report AIB-2016-09, RWTH Aachen, Germany. M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl Analyzing Runtime and Size Complexity of Integer Programs ACM Transactions on Programming Languages and Systems, 38(4), 2016. Preliminary Version F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl Lower Runtime Bounds for Integer Programs In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR '16), Coimbra, Portugal, Lecture Notes in Artificial Intelligence 9706, pages 550-567, 2016. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2016-03, RWTH Aachen, Germany. J. Hensel, J. Giesl, F. Frohn, and T. Ströder Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution In Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM '16), Vienna, Austria, Lecture Notes in Computer Science 9763, pages 234-252, 2016. Winner of the Silver Medal for the second best paper of the conference. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2016-04, RWTH Aachen, Germany. Slides of a related talk. F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder Inferring Lower Bounds for Runtime Complexity In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA '15), Warsaw, Poland, LIPIcs Leibniz International Proceedings in Informatics 36, pages 334-349, 2015. Dagstuhl Publishing. Extended version appeared as Technical Report AIB-2015-05, RWTH Aachen, Germany. Slides of a related talk. J. Giesl, F. Mesnard, A. Rubio, R. Thiemann, and J. Waldmann Termination Competition (termCOMP 2015) In Proceedings of the 25th International Conference on Automated Deduction (CADE '15), Berlin, Germany, Lecture Notes in Artificial Intelligence 9195, pages 105-108, 2015. ⒸSpringer-Verlag T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl AProVE: Termination and Memory Safety of C Programs (Competition Contribution) In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), London, UK, Lecture Notes in Computer Science 9035, pages 417-419, 2015. ⒸSpringer-Verlag T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp Proving Termination and Memory Safety for Programs with Pointer Arithmetic In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 208-223, 2014. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2014-05, RWTH Aachen, Germany. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann Proving Termination of Programs Automatically with AProVE In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 184-191, 2014. ⒸSpringer-Verlag M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl Alternating Runtime and Size Complexity Analysis of Integer Programs In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '14), Grenoble, France, Lecture Notes in Computer Science 8413, pages 140-155, 2014. ⒸSpringer-Verlag Extended version appeared as Technical Report AIB-2013-12, RWTH Aachen, Germany. Slides of a related talk. 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. The final publication is available at Springer via the DOI 10.1007/s10817-013-9277-6. 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, page 21-22, 2013. 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, Lecture Notes in Computer Science 7844 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, EPiC Series in Computing 20, pages 88-97, 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. Preliminary Version 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. Alarcon, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann Improving Context-Sensitive Dependency Pairs In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '08), Doha, Qatar, Lecture Notes in 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 Notes 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. 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. 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 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '23), Manizales, Colombia, 2023 PC Member of the 14th International Symposium on Frontiers of Combining Systems (FroCoS '23), Prague, Czech Republic, 2023 PC-Member of the Deduktionstreffen 2023, Berlin, Germany, 2023 PC-Member of the 11th International Joint Conference on Automated Reasoning (IJCAR '22), Haifa, Israel, 2022 Member of the Committee for German-Israeli Project Cooperation of the German Science Foundation, 2016 - 2021 Chair of the Herbrand Award Committee 2021 PC-Member of the 28th International Conference on Automated Deduction (CADE-28), Pittsburgh, PA, USA, 2021 PC-Member of the 13th International Symposium on Frontiers of Combining Systems (FroCoS '21), Birmingham, UK, 2021 PC-Member of the 7th International Workshop on Termination (WST '21), Pittsburgh, PA, USA, 2021 PC-Member of the 3rd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE '21), Pittsburgh, PA, USA, 2021 PC-Member of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '20), Alicante, Spain, 2020 PC-Member of the 10th International Joint Conference on Automated Reasoning (IJCAR '20), Paris, France, 2020 PC-Member of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD '20), Paris, France, 2020 PC-Member of the 17th International Workshop on Termination (WST '20), Paris, France, 2020 (cancelled) PC-Member of the 27th International Conference on Automated Deduction (CADE-27), Natal, Brazil, 2019 Member of the Herbrand Award Committee 2019 PC-Member of the 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019), Natal, Brazil, 2019 PC-Member of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD '19), Dortmund, Germany, 2019 PC-Member of the 12th International Symposium on Frontiers of Combining Systems (FroCoS '19), London, UK, 2019 PC-Member of the Deduktionstreffen 2019, Kassel, 2019 Member of the Scientific Advisory Board of the Max-Planck-Institut Informatik, Saarbrücken, Germany (2013-2018). Vice-Chair from 2015-2018. PC-Member of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '18), Awassa, Ethiopia, 2018 PC-Member of the 9th International Joint Conference on Automated Reasoning (IJCAR '18), Oxford, UK, 2018 PC-Member of the 16th International Workshop on Termination (WST '18), Oxford, UK, 2018 PC-Member of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '18), Frankfurt, Germany, 2018 PC-Member of the 12th International Workshop on Rewriting Logic and its Applications (WRLA '18), Thessaloniki, Greece, 2018 PC-Member of the Deduktionstreffen 2018, Luxembourg, 2018 PC-Member of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '17), Maun, Botswana, 2017 PC-Member of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD '17), Oxford, UK, 2017 PC-Member of the 11th International Symposium on Frontiers of Combining Systems (FroCoS '17), Brasilia, Brazil, 2017 PC-Member of the 1st International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop, Gothenburg, Sweden, 2017 PC-Member of the 8th International Joint Conference on Automated Reasoning (IJCAR '16), Coimbra, Portugal, 2016 PC-Member of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD '16), Porto, Portugal, 2016 PC-Member of the 11th International Workshop on Rewriting Logic and its Applications (WRLA '16), Eindhoven, The Netherlands, 2016 PC-Member of the Deduktionstreffen 2016, Klagenfurt, Austria, 2016 Member of the Advisory Committee of the German-Israeli Foundation (GIF), 2013-2015 PC-Member of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '15), Suva, Fiji, 2015 PC-Member of the 26th International Conference on Rewriting Techniques and Applications (RTA '15), Warsaw, Poland, 2015 PC-Member of the 10th International Symposium Frontiers of Combining Systems (FroCoS '15), Wroclaw, Poland, 2015 PC-Member of the 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '15), Siena, Italy, 2015 PC-Member of the 10th Workshop on Logical and Semantic Frameworks, with Applications (LSFA '15), Natal, Brazil, 2015 PC-Member of the Deduktionstreffen 2015, Berlin, Germany, 2015 Chair of the IFIP Working Group 1.6 on Term Rewriting, 2008 - 2014 Keynote Speaker of the International Colloquium on Implementation of Constraint and Logic Programming Systems and the Workshop on Logic-based methods in Programming Environments (CICLOPS/WLPE 2014), Vienna, Austria, 2014 PC-Member of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, 2014 PC-Member of the 14th International Workshop on Termination (WST '14), Vienna, Austria, 2014 PC-Member of the Joint Automated Reasoning Workshop and Deduktionstreffen 2014 (ARW-DT '14), Vienna, Austria, 2014 PC-Member of the 8th International Conference on Language and Automata Theory and Applications (LATA '14), Madrid, Spain, 2014 PC-Member of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR '14), Canterbury, UK, 2014 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 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 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
	Address/Office: Room 4212, 2nd Floor Building E1 (Erweiterungsbau 1) LuFGI 2 Fachgruppe Informatik RWTH Aachen Ahornstr. 55 52074 Aachen Germany Contact: Phone: +49 241 80-21230 Email: Research Topics: Program Analysis, Verification, Rewriting, Automated Deduction