T2 Temporal Prover

Last updated
T2 Temporal Prover
Original author(s) Microsoft Research
Developer(s) Microsoft
Stable release
CADE_2017 / May 30, 2017;8 years ago (2017-05-30)
Repository github.com/mmjb/T2
Written in F#
Operating system Windows, Linux (Debian, Ubuntu), macOS
Platform .NET Framework, Mono
Type Program analyzer
License MIT License
Website www.microsoft.com/en-us/research/publication/t2-temporal-property-verification/

T2 Temporal Prover is an automated program analyzer developed in the Terminator research project at Microsoft Research.

Contents

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

  1. ↑ Rob Knies. "Terminator Tackles an Impossible Task" . Retrieved 2010-05-25.
  2. ↑ "GitHub - mmjb/T2: T2 Temporal Prover". December 4, 2019 – via GitHub.

Further reading

Science-symbol-2.svg

This scientific software article is a stub. You can help Wikipedia by expanding it.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.