VMTL - Vienna Modular Termination Laboratory

VMTL is a tool for the (semi-)automatic termination analysis of rewriting systems. Currently, standard as well as context-sensitive and conditional term rewriting systems are supported.

VMTL is an implementation of the dependency pair framework, in which termination of rewrite systems is analyzed by so called dependency pair processors. The search for termination proofs in VMTL is guided by a user configurable strategy featuring hierarchical grouping of processors, time-limits on the level of processor groups as well as single processors and parallelization. In addition VMTL provides open interfaces allowing to add new dependency pair processors as well as transformations/preprocessings of rewrite systems in a modular fashion.

Two user front ends are available for VMTL. The web application (available here) provides an intuitive and easy to use graphical interface allowing to conveniently experiment with different proof strategies and transformations. The command line interface can be used more easily for batch execution and benchmark testing. It is available here.

Benchmarks of VMTL on the rewrite systems of the termination problem database can be found here.