T2 Temporal Prover
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.CS1 maint: uses authors parameter (link)
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)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.