Questions that we're frequently asked about TERMINATOR include: Question: But I thought that automatic program termination was impossible, didn't Alan Turing prove that? Answer: Program termination is an undecidable problem, i.e. TERMINATOR will never (no matter how much effort we put in to it) be able to prove the termination of every program that actually guarentees termination. However, it possible that one day we'll have tools that can prove the termination of most (or perhaps even all) programs that we might actually write. This is our goal. For more information, read this article. Question: What type of programs can TERMINATOR "handle"? Answer: This is difficult to characterize, as we are always enhancing TERMINATOR's features. Currently TERMINATOR struggles with loops and recursive functions whose termination depends on the changing shape of the heap. TERMINATOR currently only finds termination arguments expressible in linear arithmetic (where C pointer expressions are treated as mathematical variables), so it will not find termination arguments where division is important. Current research within our group is addressing this. TERMINATOR only supports sequential programs. Again, the standard answer: current research is addressing this. Furthermore, TERMINATOR cannot prove some of the notoriously difficult small examples, such as Collatz program. Question: How would a tool like TERMINATOR be used in practice? Answer: Our hope is that some future version of TERMINATOR (or a tool like it) will eventually be used routinely on new code in order to guarantee that key utilities within reactive systems (operating systems, web servers, etc) always return to their calling context. As an example, we're interested in proving that device driver dispatch routines always (eventually) return to their caller. Furthermore, we hope to create a version of TERMINATOR that supports general liveness properties (i.e. "if my code calls function A will it eventually call function B"?). This is due to the fact that all liveness properties can be converted into the problem of program termination. Question: Can I download TERMINATOR? Answer: Not yet. We're preparing a public release. Question: Which language is TERMINATOR written in? Answer: Mostly in the intersection between F# and O'Caml, some parts are written in Prolog and C++.