## References

### 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-VerlagJ. 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 VersionJ. 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-VerlagT. 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-VerlagJ. 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-VerlagJ. 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-VerlagJ. 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

back to top

### 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, 2024. To appear.

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, 2024. To appear.

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, 2024. To appear.

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, 2024. To appear.

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 VersionJ. 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 VersionF. 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 VersionF. 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 VersionF. 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 VersionM. 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-VerlagJ. 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-VerlagT. 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-VerlagL. 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 VersionM. 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 PressM. 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, GermanyP. 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-VerlagR. 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-VerlagC. 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-VerlagP. 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 VersionB. 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-VerlagC. 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-VerlagC. 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-VerlagM. 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-VerlagR. 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 VersionP. 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-VerlagJ. 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-VerlagC. 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-VerlagJ. 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 VersionM. 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-VerlagJ. 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-VerlagJ. 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 VersionJ. 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-VerlagR. 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-VerlagJ. 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.

back to top

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