References
System Description
N. Lommen and J. Giesl
AProVE (KoAT + LoAT) (Competition Contribution)
In Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '25), Hamilton, Canada, Lecture Notes in Computer Science, 2025. To appear.
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
J.-C. Kassing and J. Giesl
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
In Principles of Verification: Cycling the Probabilistic Landscape, Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 15260, pages 339-366, 2024. ⒸSpringer-Verlag
Extended version appeared at arXiv, CoRR abs/2408.06768.
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 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.