Software:T2 Temporal Prover

From HandWiki
T2 Temporal Prover
Original author(s)Microsoft Research
Developer(s)Microsoft
Stable release
CADE_2017 / May 30, 2017; 7 years ago (2017-05-30)
Repositorygithub.com/mmjb/T2
Written inF#
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/

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

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]

References

Further reading

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

External links