T2 Temporal Prover
Jump to navigation
Jump to search
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)