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-Verlag

J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
Analyzing Program Termination and Complexity Automatically with AProVE
Journal of Automated Reasoning, 58(1):3-31, 2017. ©Springer-Verlag
The final publication is available at Springer via the DOI 10.1007/s10817-016-9388-y.
Preliminary Version

J. Hensel, F. Emrich, F. Frohn, T. Ströder, and J. Giesl
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)
In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '17), Uppsala, Sweden, Lecture Notes in Computer Science 10206, pages 350-354, 2017. ©Springer-Verlag

T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl
AProVE: Termination and Memory Safety of C Programs (Competition Contribution)
In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '15), London, UK, Lecture Notes in Computer Science 9035, pages 417-419, 2015. ©Springer-Verlag

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann
Proving Termination of Programs Automatically with AProVE
In Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR '14), Vienna, Austria, Lecture Notes in Artificial Intelligence 8562, pages 184-191, 2014. ©Springer-Verlag

J. Giesl, P. Schneider-Kamp, and R. Thiemann
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework
In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06), Seattle, USA, Lecture Notes in Artificial Intelligence 4130, pages 281-286, 2006. ©Springer-Verlag

J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
Automated Termination Proofs with AProVE
In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA-04), Aachen, Germany, Lecture Notes in Computer Science 3091, pages 210-220, 2004. ©Springer-Verlag