The CondTerm Tool

Proving Conditional Termination
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv
CAV'08

Please download the following:

• The tool (including examples)
• Quantifier Elimination based on Aaron Bradely's implemenation of Cooper's algorithm. (GPL License)

Note that this tool is a proof of concept. More robust implementations of the tools are underway.