T2 Temporal Prover

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

T2 Temporal Prover

Original author(s)	Microsoft Research
Developer(s)	Microsoft
Stable release	CADE_2017 / May 30, 2017; 7 years ago (2017-05-30)
Repository	github.com/mmjb/T2
Written in	F#
Operating system	Windows, Linux (Debian, Ubuntu), macOS
Platform	.NET Framework, Mono
Type	Program analyzer
License	MIT License
Website	www.microsoft.com/en-us/research/publication/t2-temporal-property-verification/

Overview

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]