References

• System Description
• Technical Background
• Experiments

System Description

• 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. 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

• 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

• 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

• 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

• 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

• 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, 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

Technical Background

• J. Giesl, P. Schneider-Kamp, and R. Thiemann
  AProVE Technique Reference
  

• 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. 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.
  Extended version appeared at arXiv, CoRR abs/2309.00344.
  ⒸSpringer-Verlag
  

• 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
  

• 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.
  

• 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.
  

• 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.
  

• 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.
  

• 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.

• 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.

• 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.

• F. Frohn and J. Giesl
  Constant Runtime Complexity of Term Rewriting is Semi-Decidable
  Information Processing Letters, 139:18-23, 2018. ©Elsevier
  Preliminary Version

• 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

• 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.

• 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

• 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.

• 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.

• 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.

• 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.

• 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.

• 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

• 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.
  Extended version appeared as Technical Report AIB-2012-12, RWTH Aachen, Germany.

• M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
  Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  In Proceedings of the 2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in Computer Science. To appear. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2011-19, RWTH Aachen, Germany.

• 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

• 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

• L. Noschinski, F. Emmes, and J. Giesl
  The Dependency Pair Framework for Automated Complexity Analysis of Term Rewrite Systems
  In Proceedings of the 23nd 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.

• 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. Brockschmidt, C. Otto, and J. Giesl
  Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
  In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA '11), Novi Sad, Serbia LIPIcs Leibniz International Proceedings in Informatics 10, pages 155-170, 2011.
  Extended version appeared as Technical Report AIB-2011-02, RWTH Aachen, Germany.

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

• 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 Artifical Intelligence 6397, pages 217-232, 2010. ©Springer-Verlag
  Extended version appeared as Technical Report AIB-2010-14, RWTH Aachen, Germany.

• 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.

• C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
  Automated Termination Analysis of Java Bytecode by Term Rewriting
  In Proceedings of the 21th International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010.
  Extended version appeared as Technical Report AIB-2010-08, RWTH Aachen, Germany.

• 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

• 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

• 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.

• 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):1-52, 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

• 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, 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

• 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.

• 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

• 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 4407, pages 177-193, 2007. ©Springer-Verlag

• 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

• 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, R. Thiemann, and P. Schneider-Kamp
  Proving and Disproving Termination of Higher-Order Functions
  In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS '05), Vienna, Austria, Lecture Notes in Artificial Intelligence 3717, pages 216-231, 2005. ©Springer-Verlag
  Extended version available 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, R. Thiemann, and P. Schneider-Kamp
  The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
  In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '04), Montevideo, Uruguay, Lecture Notes in Artificial Intelligence 3452, pages 301-331, 2005 ©Springer-Verlag

• R. Thiemann, J. Giesl, 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
  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.

Experiments

• J.-C. Kassing and J. Giesl
  Experiments on Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2023.

• J. Hensel and J. Giesl
  Experiments on Proving Termination of C Programs with Lists
  Detailed description of our experiments to evaluate the contributions of the above paper, 2023.

• F. Frohn and J. Giesl
  Experiments on Proving Non-Termination by Acceleration Driven Clause Learning
  Detailed description of our experiments to evaluate the contributions of the above paper, 2023.

• N. Lommen, F. Meyer, and J. Giesl
  Experiments on Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
  Detailed description of our experiments to evaluate the contributions of the above paper, 2022.

• F. Frohn and J. Giesl
  Experiments on Proving Non-Termination and Lower Runtime Bounds with LoAT
  Detailed description of our experiments to evaluate the contributions of the above paper, 2022.

• J. Giesl, N. Lommen, M. Hark, and F. Meyer
  Experiments on Improving Automatic Complexity Analysis of Integer Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2022.

• F. Meyer, M. Hark, and J. Giesl
  Experiments on Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
  Detailed description of our experiments to evaluate the contributions of the above paper, 2021.

• F. Frohn, M. Naaf, M. Brockschmidt, and J. Giesl
  Experiments on Inferring Lower Runtime Bounds for Integer Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2020.

• F. Frohn and J. Giesl
  Experiments on Proving Non-Termination via Loop Acceleration
  Detailed description of our experiments to evaluate the contributions of the above paper, 2019.

• J. Giesl, P. Giesl, and M. Hark
  Experiments on Computing Expected Runtimes for Constant Probability Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2019.

• J. Hensel, J. Giesl, F. Frohn, and T. Ströder
  Experiments on Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution
  Detailed description of our experiments to evaluate the contributions of the above paper, 2018.

• F. Frohn and J. Giesl
  Experiments on Complexity Analysis for Java with AProVE
  Detailed description of our experiments to evaluate the contributions of the above paper, 2017.

• M. Naaf, F. Frohn, M. Brockschmidt, C. Fuhs, and J. Giesl
  Experiments on Complexity Analysis for Term Rewriting by Integer Transition Systems
  Detailed description of our experiments to evaluate the contributions of the above paper, 2017.

• F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
  Experiments on Lower Bounds for Runtime Complexity of Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2017.

• F. Frohn and J. Giesl
  Experiments on Analyzing Runtime Complexity via Innermost Runtime Complexity
  Detailed description of our experiments to evaluate the contributions of the above paper, 2017.

• T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, P. Schneider-Kamp, and C. Aschermann
  Experiments on Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
  Detailed description of our experiments to evaluate the contributions of the above paper, 2016.

• M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl
  Experiments on Analyzing Runtime and Size Complexity of Integer Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2016.

• F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl
  Experiments on Lower Runtime Bounds for Integer Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2016.

• J. Hensel, J. Giesl, F. Frohn, and T. Ströder
  Experiments on Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
  Detailed description of our experiments to evaluate the contributions of the above paper, 2016.

• F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder
  Experiments on Inferring Lower Bounds for Runtime Complexity
  Detailed description of our experiments to evaluate the contributions of the above paper, 2015.

• T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel, and P. Schneider-Kamp
  Experiments on Proving Termination and Memory Safety for Programs with Pointer Arithmetic
  Detailed description of our experiments to evaluate the contributions of the above paper, 2014.

• M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl
  Experiments on Alternating Runtime and Size Complexity Analysis of Integer Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2014.

• L. Noschinski, F. Emmes, and J. Giesl
  Experiments on Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2013.

• M. Brockschmidt, R. Musiol, C. Otto, and J. Giesl
  Experiments on Automated Termination Proofs for Java Programs with Cyclic Data
  Detailed description of our experiments to evaluate the contributions of the above paper, 2012.

• F. Emmes, T. Enger, and J. Giesl
  Experiments on Proving Non-Looping Non-Termination Automatically
  Detailed description of our experiments to evaluate the contributions of the above paper, 2012.

• J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs
  Experiments on Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2012.

• M. Codish, J. Giesl, P. Schneider-Kamp, and R. Thiemann
  Experiments on SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2012.

• M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
  Experiments on Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode
  Detailed description of our experiments to evaluate the contributions of the above paper, 2011.

• C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, and S. Swiderski
  Experiments on Proving Termination by Dependency Pairs and Inductive Theorem Proving
  Detailed description of our experiments to evaluate the contributions of the above paper, 2011.

• L. Noschinski, F. Emmes, and J. Giesl
  Experiments on The Dependency Pair Framework for Automated Complexity Analysis of Term Rewrite Systems
  Detailed description of our experiments to evaluate the contributions of the above paper, 2011.

• M. Brockschmidt, C. Otto, and J. Giesl
  Experiments on Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2011.

• M. Codish, I. Gonopolskiy, A. Ben-Amram, C. Fuhs, and J. Giesl
  Experiments on SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers
  Detailed description of our experiments to evaluate the contributions of the above paper, 2011.

• M. Codish, C. Fuhs, J. Giesl, and P. Schneider-Kamp
  Experiments on Lazy Abstraction for Size-Change Termination
  Detailed description of our experiments to evaluate the contributions of the above paper, 2010.

• C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
  Experiments on Automated Termination Analysis of Java Bytecode by Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2010.

• T. Ströder, P. Schneider-Kamp, and J. Giesl
  Experiments on Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
  Detailed description of our experiments to evaluate the contributions of the above paper, 2010.

• S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. Schneider-Kamp
  Experiments on Termination Analysis by Dependency Pairs and Inductive Theorem Proving
  Detailed description of our experiments to evaluate the contributions of the above paper, 2009.

• C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke
  Experiments on Proving Termination of Integer Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2009.

• B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutierrez, S. Lucas, P. Schneider-Kamp, and R. Thiemann
  Experiments on Improving Context-Sensitive Dependency Pairs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2008.

• P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
  Experiments on Automated Termination Proofs for Logic Programs by Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2008.

• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  Experiments on Maximal Termination
  Detailed description of our experiments to evaluate the contributions of the above paper, 2008.

• R. Thiemann, J. Giesl, and P. Schneider-Kamp
  Experiments on Deciding Innermost Loops
  Detailed description of our experiments to evaluate the contributions of the above paper, 2008.

• C. Fuhs, R. Navarro, C. Otto, J. Giesl, S. Lucas, P. Schneider-Kamp
  Experiments on Search Techniques for Rational Polynomial Orders
  Detailed description of our experiments to evaluate the contributions of the above paper, 2008.

• P. Schneider-Kamp, R. Thiemann, E. Annov, M. Codish, J. Giesl
  Experiments on Proving Termination using Recursive Path Orders and SAT Solving
  Detailed description of our experiments to evaluate the contributions of the above paper, 2007.

• J. Giesl, R. Thiemann, S. Swiderski, and P. Schneider-Kamp
  Experiments on Proving Termination by Bounded Increase
  Detailed description of our experiments to evaluate the contributions of the above paper, 2007.

• C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, and H. Zankl
  Experiments on SAT Solving for Termination Analysis with Polynomial Interpretations
  Detailed description of our experiments to evaluate the contributions of the above paper, 2007.

• P. Schneider-Kamp, J. Giesl, A. Serebrenik, and R. Thiemann
  Experiments on Automated Termination Analysis for Logic Programs by Term Rewriting
  Detailed description of our experiments to evaluate the contributions of the above paper, 2006.

• J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
  Experiments on Mechanizing and Improving Dependency Pairs
  Detailed description of our experiments to evaluate the contributions of the above paper, 2006.

• M. Codish, P. Schneider-Kamp, V. Lagoon, R. Thiemann, and J. Giesl
  Experiments on SAT Solving for Argument Filterings
  Detailed description of our experiments to evaluate the contributions of the above paper, 2006.

• J. Giesl, S. Swiderski, P. Schneider-Kamp, and R. Thiemann
  Experiments on Automated Termination Analysis for Haskell
  Detailed description of our experiments to evaluate the contributions of the above paper, 2006 and 2010.

• J. Giesl, R. Thiemann, and P. Schneider-Kamp
  Experiments on Proving and Disproving Termination of Higher-Order Functions
  Detailed description of our experiments to evaluate the contributions of the above paper, 2005.