left

Techniques

right
AProVE Help SystemReferencesTechniques

Most of the techniques used in AProVE are described in one or more of the following papers. The table is sorted chronologically.

TGSK '04 R. Thiemann, J. Giesl, P. Schneider-Kamp
Improved Modular Termination Proofs Using Dependency Pairs
In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR 2004), Cork, Ireland, Lecture Notes in Artificial Intelligence 3097, pages 75-90, 2004. ©Springer-Verlag
HM '04 N. Hirokawa and A. Middeldorp
Dependency Pairs Revisited
In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA '04), Aachen, Germany, Lecture Notes in Computer Science 3091, pages 249-268, 2004. ©Springer-Verlag
Zan '04 H. Zantema
TORPA: Termination of Rewriting Proved Automatically In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA-04), Aachen, Germany, Lecture Notes in Computer Science 3091, pages 95-104, 2004. ©Springer-Verlag
Has '04 C. Haselbach
Transformation Techniques to Verify Imperative and Functional Programs
Diploma-Thesis, RWTH Aachen
GTSKF '03b J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
Mechanizing Dependency Pairs
Technical Report AIB-2003-08, RWTH Aachen, Germany.
GTSKF '03 J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke
Improving Dependency Pairs
In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), Almaty, Kazakhstan, Lecture Notes in Artificial Intelligence 2850, pages 167-182, 2003. ©Springer-Verlag
Extended version
available as Technical Report AIB-2003-04, RWTH Aachen, Germany.
HM '03 N. Hirokawa and A. Middeldorp
Automating the dependency pair method
In Proceedings of the 19th International Conference on Automated Deduction (CADE '03), Miami, Florida, USA, Lecture Notes in Computer Science 2741, 2003. ©Springer-Verlag
TG '03 R. Thiemann and J. Giesl
Size-Change Termination for Term Rewriting
In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA '03), Valencia, Spain, Lecture Notes in Computer Science 2706, pages 264-278, 2003. ©Springer-Verlag
Extended version available as Technical Report AIB-2003-02, RWTH Aachen, Germany.
GZ '03 J. Giesl and H. Zantema
Liveness in Rewriting
In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA '03), Valencia, Spain, Lecture Notes in Computer Science 2706, pages 321-336, 2003. ©Springer-Verlag
Extended version available as Technical Report AIB-2002-1, RWTH Aachen, Germany and as CS-Report 01-03, Technical University Eindhoven, The Netherlands.
GM '02 J. Giesl and Aart Middeldorp
Innermost Termination of Context-Sensitive Rewriting
In Proceedings of the 6th International Conference on Developments in Language Theory (DLT 2002), Kyoto, Japan, Lecture Notes in Computer Science 2450, pages 231-244, 2003. ©Springer-Verlag
Ohl '01 Enno Ohlebusch
Termination of Logic Programs: Transformational Methods Revisited
In AAECC 12, 73-116 (2001) © Springer-Verlag
AG '00 T. Arts and J. Giesl
Termination of Term Rewriting Using Dependency Pairs
In Theoretical Computer Science 236, pages 133-178, 2000. ©Springer-Verlag
Gra '96 B. Gramlich
On Proving Termination by Innermost Termination
In Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA '96), Lecture Notes in Computer Science 1103, pages 97-107, 1996. ©Springer-Verlag
Zan '95 H. Zantema
Termination of term rewriting by semantic labelling,
Fundamenta Informaticae, 24:89-105, 1995.
Gie '95 J. Giesl
Automatisierung von Terminierungsbeweisen für rekursiv definierte Algorithmen.
Dissertation, Infix-Verlag, Sankt Augustin, 1995.