Hubbry Logo
T2 Temporal ProverT2 Temporal ProverMain
Open search
T2 Temporal Prover
Community hub
T2 Temporal Prover
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
T2 Temporal Prover
from Wikipedia
T2 Temporal Prover
Original authorMicrosoft Research
DeveloperMicrosoft
Stable release
CADE_2017 / May 30, 2017; 8 years ago (2017-05-30)
Written inC, F#
Operating systemWindows, Linux (Debian, Ubuntu), macOS
Platform.NET Framework, Mono
TypeProgram analyzer
LicenseMIT License
Websitewww.microsoft.com/en-us/research/publication/t2-temporal-property-verification/
Repositorygithub.com/mmjb/T2

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

Overview

[edit]

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]

References

[edit]

Further reading

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia
Add your contribution
Related Hubs
User Avatar
No comments yet.