T2 Temporal Prover
Original author(s)Microsoft Research
Stable release
CADE_2017 / May 30, 2017; 6 years ago (2017-05-30)
Written inF#
Operating systemWindows, Linux (Debian, Ubuntu), macOS
Platform.NET Framework, Mono
TypeProgram analyzer
LicenseMIT License

T2 Temporal Prover is an automated program analyzer developed in the Terminator research project at Microsoft Research.


T2 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.[1] It provides a solution which is sound, meaning that when it states that a program does always terminate, the result is dependable.

The source code is licensed under MIT License and hosted on GitHub.[2]


  1. ^ Rob Knies. "Terminator Tackles an Impossible Task". Retrieved 2010-05-25.
  2. ^ "GitHub - mmjb/T2: T2 Temporal Prover". December 4, 2019 – via GitHub.

Further reading