1.3 KiB
| title | chunk | source | category | tags | date_saved | instance |
|---|---|---|---|---|---|---|
| T2 Temporal Prover | 1/1 | https://en.wikipedia.org/wiki/T2_Temporal_Prover | reference | science, encyclopedia | 2026-05-05T12:18:19.726352+00:00 | kb-cron |
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. 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.
== References ==
== 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)