T2 Temporal Prover is an automatedprogram analyzer developed in theTerminator research project atMicrosoft Research.

T2 aims to find whether a program can run infinitely (called atermination 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 thehalting problem for particular cases, since the general problem isundecidable.^[1] It provides a solution which issound, meaning that when it states that a program does always terminate, the result is dependable.

The source code is licensed underMIT License and hosted onGitHub.^[2]

• Marc Brockschmidt; Byron Cook; Samin Ishtiaq; Heidy Khlaaf; Nir Piterman (2016). "T2: Temporal Property Verification".Proceedings of TACAS'16.Springer.arXiv:1512.08689.

• T2 Temporal Logic Prover onGitHub
• T2: Temporal Property Verification publication at Microsoft Research
• Terminator Research Project at theWayback Machine (archived October 4, 2013)

ThisMicrosoft Windowssoftware-related article is astub. You can help Wikipedia byadding missing information.

• v
• t
• e

Thisscientific software article is astub. You can help Wikipedia byadding missing information.

• v
• t
• e

• Free software programmed in C
• Microsoft free software
• Microsoft Research
• Software that uses Mono (software)
• Software using the MIT license
• Windows software stubs
• Science software stubs

• Webarchive template wayback links
• All stub articles