T2 Temporal Prover

(Redirected from Microsoft Terminator)

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; 6 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/

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

  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 edit

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

External links edit