T2 Temporal Prover
| T2 Temporal Prover | |
|---|---|
| Original author | Microsoft Research |
| Developer | Microsoft |
| Stable release | CADE_2017
/ May 30, 2017 |
| Repository | github |
| Written in | C, F# |
| Engine | |
| Operating system | Windows, Linux (Debian, Ubuntu), macOS |
| Platform | .NET Framework, Mono |
| Type | Program analyzer |
| License | MIT License |
| Website | www |
Lua error in mw.title.lua at line 392: bad argument #2 to 'title.new' (unrecognized namespace name 'Portal'). T2 Temporal Prover is an automated program analyzer developed in the Terminator research project at Microsoft Research.
Overview
[edit | edit source]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 | edit source]Further reading
[edit | edit source]- Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
External links
[edit | edit source]- 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)
