| Original author(s) | Microsoft Research |
|---|---|
| Developer(s) | Microsoft |
| Stable release | CADE_2017
/ May 30, 2017 |
| Repository |
github |
| Written in | F# |
| Operating system | Windows, Linux ( Debian, Ubuntu), macOS |
| Platform | .NET Framework, Mono |
| Type | Program analyzer |
| License | MIT License |
| Website |
www |
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
- ^ Rob Knies. "Terminator Tackles an Impossible Task". Retrieved 2010-05-25.
- ^ "GitHub - mmjb/T2: T2 Temporal Prover". December 4, 2019 – via GitHub.
Further reading
- 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
- T2 Temporal Logic Prover on GitHub
- T2: Temporal Property Verification publication at Microsoft Research
- Terminator Research Project at the Wayback Machine (archived October 4, 2013)
| Main projects |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs applied research |
| ||||||||||||||
 | This Microsoft Windows software-related article is a stub. You can help Wikipedia by expanding it. |
 | This scientific software article is a stub. You can help Wikipedia by expanding it. |
| Original author(s) | Microsoft Research |
|---|---|
| Developer(s) | Microsoft |
| Stable release | CADE_2017
/ May 30, 2017 |
| Repository |
github |
| Written in | F# |
| Operating system | Windows, Linux ( Debian, Ubuntu), macOS |
| Platform | .NET Framework, Mono |
| Type | Program analyzer |
| License | MIT License |
| Website |
www |
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
- ^ Rob Knies. "Terminator Tackles an Impossible Task". Retrieved 2010-05-25.
- ^ "GitHub - mmjb/T2: T2 Temporal Prover". December 4, 2019 – via GitHub.
Further reading
- 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
- T2 Temporal Logic Prover on GitHub
- T2: Temporal Property Verification publication at Microsoft Research
- Terminator Research Project at the Wayback Machine (archived October 4, 2013)
| Overview | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Software |
| ||||||||||||
| Licenses | |||||||||||||
| Forges | |||||||||||||
| Related | |||||||||||||
| Main projects |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs applied research |
| ||||||||||||||
|
| This Microsoft Windows software-related article is a stub. You can help Wikipedia by expanding it. |
|
| This scientific software article is a stub. You can help Wikipedia by expanding it. |