
References
System Description
 J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn,
C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. SchneiderKamp,
T. Ströder, S. Swiderski, and R. Thiemann
Analyzing Program Termination and Complexity
Automatically with AProVE
Journal of Automated Reasoning, 58(1):331, 2017.
©SpringerVerlag
The final publication is available at Springer via the DOI 10.1007/s108170169388y.
Preliminary Version
 J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl
AProVE: Proving
and Disproving Termination of
MemoryManipulating 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 350354, 2017. ©SpringerVerlag
 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 417419, 2015. ©SpringerVerlag
 J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto,
M. Plücker, P. SchneiderKamp, 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 184191, 2014. ©SpringerVerlag
 J. Giesl, P. SchneiderKamp, 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 281286, 2006. ©SpringerVerlag
 J. Giesl, R. Thiemann, P. SchneiderKamp, and S. Falke
Automated Termination Proofs with AProVE
In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA04),
Aachen, Germany, Lecture Notes in Computer Science 3091, pages 210220, 2004.
©SpringerVerlag
Technical Background
 J. Giesl, P. SchneiderKamp, and R. Thiemann
AProVE Technique Reference
F. Frohn and J. Giesl
Proving NonTermination via Loop Acceleration
In Proceedings of the 19th International Conference on Formal Methods in
ComputerAided Design
(FMCAD '19), San Jose, CA, USA, 2019. To appear.
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 269286, 2019.
ⒸSpringerVerlag
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 426444, 2019.
ⒸSpringerVerlag
Extended
version appeared at arXiv, CoRR abs/1905.08664.
F. Frohn and J. Giesl
Constant Runtime Complexity of Term Rewriting is
SemiDecidable
Information Processing Letters, 139:1823, 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:105130, 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 85101,
2017. Winner of the Best Tool Paper Award of the conference. ©SpringerVerlag
Extended
version appeared as Technical Report AIB201704, 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 132150,
2017. ©SpringerVerlag
Extended
version appeared as Technical Report AIB201705, 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):121163, 2017.
©SpringerVerlag
The final publication is available at Springer via the
DOI 10.1007/s108170169397x.
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 249268, 2017.
Extended
version appeared as Technical Report AIB201702, RWTH Aachen University, Germany.
 T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs,
J. Hensel, P. SchneiderKamp, and
C. Aschermann
Automatically Proving Termination and Memory Safety for
Programs with Pointer Arithmetic
Journal of Automated Reasoning, 58(1):3365, 2017.
©SpringerVerlag
The final publication is available at Springer via the
DOI 10.1007/s108170169389x.
Preliminary
Version
Extended version appeared as Technical Report AIB201609, 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 550567, 2016. ©SpringerVerlag
Extended version appeared as Technical Report AIB201603, 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 234252, 2016. Winner of the Silver Medal
for the second best paper of the conference. ©SpringerVerlag
Extended version appeared as Technical Report AIB201604, 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 334349, 2015. Dagstuhl Publishing.
Extended version appeared as Technical Report AIB201505, RWTH Aachen, Germany.
 T. Ströder, J. Giesl, M. Brockschmidt, F. Frohn, C. Fuhs, J. Hensel,
and P. SchneiderKamp
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 208223, 2014. ©SpringerVerlag
Extended version appeared as Technical Report AIB201405, 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 140155, 2014. ©SpringerVerlag
Extended version appeared as Technical Report AIB201312, 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):2756, 2013. ©SpringerVerlag.
The final publication is available at Springer via the DOI 10.1007/s1081701392776.
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
105122, 2012. ©SpringerVerlag
Extended version appeared as Technical Report AIB201206, RWTH Aachen, Germany.
 F. Emmes, T. Enger, and J. Giesl
Proving NonLooping NonTermination
Automatically
In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR '12), Manchester, UK,
Lecture Notes in Artificial Intelligence 7364, pages 225240, 2012. ©SpringerVerlag
 J. Giesl, T. Ströder, P. SchneiderKamp, 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 112,
2012. ©ACM Press.
Extended version appeared as Technical Report AIB201212, RWTH Aachen, Germany.
 M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl
Automated Detection of NonTermination and NullPointerExceptions for Java Bytecode
In Proceedings of the 2nd International Conference on Formal Verification of
ObjectOriented Software (FoVeOOS '11), Turin, Italy, Lecture Notes in
Computer Science. To appear. ©SpringerVerlag
Extended version appeared as Technical Report AIB201119, RWTH Aachen, Germany.
 C. Fuhs, J. Giesl, M. Parting, P. SchneiderKamp, and S. Swiderski
Proving Termination by Dependency Pairs and Inductive Theorem Proving
Journal of Automated Reasoning, 47(2):133160, 2011. ©SpringerVerlag
 T. Ströder, F. Emmes, P. SchneiderKamp, 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 LogicBased Program Synthesis and Transformation (LOPSTR '11), Odense, Denmark,
Lecture Notes in Computer Science 7225, pages 237252, 2012. ©SpringerVerlag
Extended version appeared as Technical Report AIB201108, RWTH Aachen, Germany.
 M. Codish, J. Giesl, P. SchneiderKamp, and R. Thiemann
SAT Solving for Termination Proofs with Recursive
Path Orders and Dependency Pairs
Journal of Automated Reasoning, 49(1):5393, 2012. ©SpringerVerlag
 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 422438, 2011. ©SpringerVerlag
Extended version appeared as
Technical Report AIB201103, RWTH Aachen, Germany.
 J. Giesl, M. Raffelsieper, P. SchneiderKamp, 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 155170, 2011.
Extended version appeared as
Technical Report AIB201102, RWTH Aachen, Germany.
 M. Codish, I. Gonopolskiy, A. BenAmram, C. Fuhs, and J. Giesl
SATBased 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(45),
503520, 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 1737, 2010. ©SpringerVerlag
Extended version appeared as Technical Report AIB201015, RWTH Aachen, Germany.
 M. Codish, C. Fuhs, J. Giesl, and P. SchneiderKamp
Lazy Abstraction for SizeChange 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 217232, 2010. ©SpringerVerlag
Extended version appeared as Technical Report AIB201014, RWTH Aachen, Germany.
 T. Ströder, P. SchneiderKamp, and J. Giesl
Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
In Proceedings of the 20th International Symposium on LogicBased Program Synthesis and Transformation (LOPSTR '10),
Hagenberg, Austria, Lecture Notes in Computer Science 6564, pages 184199,
2011. ©SpringerVerlag
Extended version appeared as Technical Report AIB201012, 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 259276, 2010.
Extended version appeared as Technical Report AIB201008, RWTH Aachen, Germany.
 P. SchneiderKamp, 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(46):365381, 2010.
©Cambridge University Press.
Extended version appeared as Technical Report AIB201010, RWTH Aachen, Germany
 P. SchneiderKamp, J. Giesl, and M. T. Nguyen
The Dependency Triple Framework for Termination of Logic Programs
In Proceedings of the 19th International Symposium on
LogicBased Program Synthesis and Transformation (LOPSTR '09), Coimbra, Portugal,
Lecture Notes in Computer Science 6037, pages 3751, 2010. ©SpringerVerlag
 R. Thiemann, C. Sternagel, J. Giesl, and P. SchneiderKamp
Loops under Strategies ... Continued
In Proceedings of the International Workshop on Strategies in Rewriting, Proving, and Programming (IWS '10), Edinburgh, UK, EPTCS 44, pages 5165, 2010.
 S. Swiderski, M. Parting, J. Giesl, C. Fuhs, and P. SchneiderKamp
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 322338, 2009. ©SpringerVerlag
 C. Fuhs, J. Giesl, M. Plücker, P. SchneiderKamp, 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 3247, 2009. ©SpringerVerlag
 P. SchneiderKamp, J. Giesl, A. Serebrenik, and R. Thiemann
Automated Termination Proofs for Logic Programs by Term Rewriting
ACM Transactions on Computational Logic, 11(1):152, 2009.
Preliminary Version
 B. Alarcón, F. Emmes, C. Fuhs, J. Giesl, R. Gutiérrez, S. Lucas, P. SchneiderKamp, and R. Thiemann
Improving ContextSensitive 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 636651, 2008. ©SpringerVerlag
 C. Fuhs, J. Giesl, A. Middeldorp, P. SchneiderKamp, 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 110125, 2008. ©SpringerVerlag
Extended version appeared as Technical Report AIB200803, RWTH Aachen, Germany.
 R.
Thiemann, J. Giesl, and P. SchneiderKamp
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 366380, 2008. ©SpringerVerlag
 C. Fuhs, R. NavarroMarset, C. Otto, J. Giesl, S. Lucas, P. SchneiderKamp
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 109124, 2008. ©SpringerVerlag
 M. T. Nguyen, J. Giesl, P. SchneiderKamp, and D. De Schreye
Termination Analysis of Logic Programs based on Dependency Graphs
In
Proceedings of the 17th International Symposium on LogicBased Program
Synthesis and Transformation (LOPSTR '07), Kongens Lyngby, Denmark, Lecture
Notes in Computer Science 4915, pages 822, 2008. ©SpringerVerlag
 R. Thiemann, H. Zantema, J. Giesl, and P. SchneiderKamp
Adding Constants to String Rewriting
Applicable Algebra in Engineering, Communication and Computing, 19(1):2738, 2008.
SpringerVerlag.
Preliminary Version
 P. SchneiderKamp, 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
267282, 2007. ©SpringerVerlag
 J. Giesl, R. Thiemann, S. Swiderski, and P. SchneiderKamp
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
443459, 2007. ©SpringerVerlag
Extended version appeared as Technical Report AIB200703, RWTH Aachen, Germany.
 P. SchneiderKamp, J. Giesl, A. Serebrenik, and R. Thiemann
Automated Termination Analysis for Logic Programs by Term Rewriting
In Proceedings of the 16th International Symposium on LogicBased Program Synthesis
and Transformation (LOPSTR '06), Venice, Italy, Lecture Notes in Computer Science
4407, pages 177193, 2007. ©SpringerVerlag
 C. Fuhs, J. Giesl, A. Middeldorp, P. SchneiderKamp, 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 177193, 2007. ©SpringerVerlag
 J. Giesl, R. Thiemann, P. SchneiderKamp, and S. Falke
Mechanizing and Improving Dependency Pairs
Journal of Automated Reasoning, 37(3): 155203, 2006. SpringerVerlag.
Preliminary Version
 M. Codish, P. SchneiderKamp, 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 3044, 2006. ©SpringerVerlag
 J. Giesl, S. Swiderski, P. SchneiderKamp, 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 (RTA06), Seattle, USA, Lecture
Notes in Computer Science 4098, pages 297312, 2006. ©SpringerVerlag
 J. Giesl, R. Thiemann, and P. SchneiderKamp
Proving and Disproving Termination of HigherOrder Functions
In Proceedings of the 5th International Workshop on Frontiers of Combining Systems
(FroCoS '05), Vienna, Austria, Lecture Notes in Artificial
Intelligence 3717, pages 216231, 2005.
©SpringerVerlag
Extended version
available as Technical Report AIB200503, RWTH Aachen, Germany.
 R. Thiemann and J. Giesl
The SizeChange Principle and Dependency Pairs for Termination of Term Rewriting
Applicable Algebra in Engineering, Communication and Computing, 16(4):229270, 2005. ©SpringerVerlag
Preliminary Version

J. Giesl, R. Thiemann, and P. SchneiderKamp
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 301331, 2005
©SpringerVerlag
 R. Thiemann, J. Giesl, P. SchneiderKamp
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 7590, 2004.
©SpringerVerlag
 J. Giesl, R. Thiemann, P. SchneiderKamp, 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 167182, 2003.
©SpringerVerlag
Extended version available as Technical Report AIB200304, RWTH Aachen, Germany.
Experiments
F. Frohn and J. Giesl
Experiments on Proving NonTermination 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. SchneiderKamp, 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. SchneiderKamp
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 NonLooping NonTermination
Automatically
Detailed description of our experiments to evaluate the contributions of the above paper, 2012.
 J. Giesl, T. Ströder, P. SchneiderKamp, 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. SchneiderKamp, 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 NonTermination 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. SchneiderKamp, 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. BenAmram, C. Fuhs, and J. Giesl
Experiments on
SATBased 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. SchneiderKamp
Experiments on
Lazy Abstraction for SizeChange 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. SchneiderKamp, 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. SchneiderKamp
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. SchneiderKamp, 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. SchneiderKamp, and R. Thiemann
Experiments on Improving ContextSensitive Dependency Pairs
Detailed description of our experiments to evaluate the contributions of the above paper, 2008.
 P. SchneiderKamp, 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. SchneiderKamp, 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. SchneiderKamp
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. SchneiderKamp
Experiments on Search Techniques for Rational Polynomial Orders
Detailed description of our experiments to evaluate the contributions of the above paper, 2008.
 P. SchneiderKamp, 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. SchneiderKamp
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. SchneiderKamp, 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. SchneiderKamp, 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. SchneiderKamp, 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. SchneiderKamp, 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. SchneiderKamp, 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. SchneiderKamp
Experiments on Proving and Disproving Termination of HigherOrder Functions
Detailed description of our experiments to evaluate the contributions of the above paper, 2005.
