NTI: Non-Termination Inference

NTI is a tool that can be used for automated non-termination proofs of term rewrite systems, string rewrite systems and logic programs. It implements the "unfold and infer" technique described in the papers below. When a proof of non-termination is successfully performed, NTI provides an example of a non-terminating term, string or atomic query (depending on the paradigm). Only standard rewriting is implemented for the moment.

NTI has been totally rewritten in Java (the former 2008 version was fully written in C++).

Tool

Papers

Experiments


Valid XHTML 1.0 Strict