TPA
(Termination Proved Automatically)
TPA is a tool for proving (relative) termination of term rewrite systems (TRS) fully automatically.
[ About TPA | News | Download | TPA in action! | FAQ | Links | Contact ]
- About TPA - what is it all about.
- News - stay informed!
- Download - you can download the latest version of TPA here.
- TPA in action! - here you can see the results of application of TPA to some systems.
- FAQ - Frequently Asked Questions.
- TPA's friends - other termination tools and sites of interest.
- Contact - all comments/suggestions/bug reports/... are very welcome!
About TPA
TPA is a tool for proving termination and relative termination of term rewrite systems automatically.
It is developed by Adam Koprowski at TU/e within
TORPA project. TPA has some novel features compared
with other termination provers. It uses the following termination proving techniques:
- Polynomial and matrix interpretations,
- Semantic and predictive labeling (both with booleans and with natural numbers),
- Recursive path ordering (RPO),
- Dependency pair transformation (DP),
- Dummy elimination
You can download a document with a more detailed list of techniques used by TPA in the download section.
News
| 06.2007 |
TPA with CoLoR just won the certified termination competition!
See here for detailed results.
|
| 12.06.2006 |
Version 1.1 of the tool available for download as well as a concise description of the techniques it is using. |
| 9.02.2006 |
Version 1.0b of the tool available for download. |
| 13.05.2005 |
Web-page of TPA launched! |
| 11.04.2005 |
TPA takes part in Termination competition 2005
run at the RTA'05 conference. It got
3rd place out of 6 participants.
Considering that the first two tools were AProVE and
TTT it was in a very good company!
|
Download
Here you can download TPA. Please note that this is a rather archaic version of the tool. If you are
interested in acquiring a newer version please contact me.
Concise description of techniques used by TPA.
TPA in action!
Here you can see few proofs as produced by TPA. The input files conform to the TRS
format.
- SUBST (input file)- the system describing the process of substitution in combinatory categorical logic. Using
semantic labelling with natural numbers TPA is the first tool to show termination of this system.
- Readers-Writers (input file) and
Cars over the bridge (input file) - two examples of termination proofs obtained
in the process of verification of liveness properties. Both are relative termination proofs.
- GCD (input file) - a possible coding of the
GCD computation. One of the systems that during the
termination competition 2005 no other tool except TPA could solve.
FAQ
?There are many existing provers for termination of term
rewrite systems, why make yet another one?
The main motivation to write TPA was to:
- handle not only termination but also relative termination,
- use the technique of semantic and predictive labeling with natural numbers,
- investigate applicability of methods for proving termination to establish liveness properties and
- to focus on certification of termination results. This is accomplished by collaboration
with the CoLoR project.
?What programming language has been used to develop TPA?
TPA is fully written in Objective Caml. Caml is a modern functional
programming language that proved to be the perfect choice due to its functional nature (expressiveness,
strong typing system) and very effective compiler.
TPA's friends
Other termination tools (in alphabetical order):
Other pages about termination of rewriting proved automatically:
Contact
For any questions, bug reports, comments etc. please contact: 
.
[ About TPA | News | Download | TPA in action! | FAQ | Links | Contact ]