Terminator, a research project at Microsoft Research, is an automated program analyzer that aims to find whether a program can run infinitely (called a termination analysis). It supports nested loops and recursive functions, pointers and side-effects, and function-pointers as well as concurrent programs. Like all programs for termination analysis it tries to solve the halting problem for particular cases, since the general problem is undecidable. It provides a solution which is sound, meaning that when it states that a program does always terminate, the result is dependable.
- Rob Knies. "Terminator Tackles an Impossible Task". Retrieved 2010-05-25.
- Terminator Research Project at the Wayback Machine (archived 2013-10-04)
- T2: Temporal Property Verification publication at Microsoft Research
- T2 Temporal Logic Prover on GitHub
|This Microsoft Windows software-related article is a stub. You can help Wikipedia by expanding it.|