TTT2 - EuroProofNet/ProgramVerification GitHub Wiki

The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of term rewrite systems. It is the completely redesigned successor of TTT.

What inputs are supported?

TTT2 accepts the input format for Term Rewrite Systems as specified in TPDB (XML and old TRS format). Moreover, also several variations for relative termination or strategy annotations (innermost rewriting,...) are accepted.

What properties can be verified?

termination and non-termination

What are the tool’s main techniques for the supported (input, property) pairs?

Dependency Pair framework, various interpretation methods, transformation methods, ... (for a complete list call the executable with ./ttt2 --processors)

What external tools are used? (e.g., compilers, SMT solvers)

  • SAT solvers: MiniSat, MiniSat+, PicoSAT
  • SMT solvers: MiniSMT (which is part of TTT2), in some cases Z3 (others can be used via flags if installed on user system)
  • nonreachability analysis: nonreach can be used in the strategy to improve edge estimation

What is the tool’s URL?

Example(s)

The termination community maintains a database with thousands of examples, called Termination Problem DataBase (TPDB).

Other relevant information

For some methods (LPO, KBO, polynomial interpretations, matrix interpretations, weighted path order) TTT2 can check specific handwritten proofs and verify them afterwards with CeTA. Furthermore, via a config file one can specify complex strategies for TTT2 (see ./ttt2 --help for more information). In case of bugs please contact the mailing list ttt2 at informatik dot uibk dot ac dot at.

References

  • Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp Tyrolean Termination Tool 2 In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), LNCS 5595, pp. 295 – 304, 2009. DOI