T2 Temporal Prover is an automated program analyzer developed in the ''Terminator'' research project at

Microsoft Research Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...

Overview

T2 aims to find whether a program can run infinitely (called a

termination analysis In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for ''each'' input. This means to determine whether the input program computes a ''total'' function. It is ...

). 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 In computability theory (computer science), computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run for ...

for particular cases, since the general problem is undecidable. It provides a solution which is

sound In physics, sound is a vibration that propagates as an acoustic wave through a transmission medium such as a gas, liquid or solid. In human physiology and psychology, sound is the ''reception'' of such waves and their ''perception'' by the br ...

, meaning that when it states that a program does always terminate, the result is dependable. The source code is licensed under

MIT License The MIT License is a permissive software license originating at the Massachusetts Institute of Technology (MIT) in the late 1980s. As a permissive license, it puts very few restrictions on reuse and therefore has high license compatibility. Unl ...

and hosted on

GitHub GitHub () is a Proprietary software, proprietary developer platform that allows developers to create, store, manage, and share their code. It uses Git to provide distributed version control and GitHub itself provides access control, bug trackin ...

References

External links

T2 Temporal Logic Prover
on

T2: Temporal Property Verification publication
at Microsoft Research * Free and open-source software Microsoft free software Microsoft Research Software that uses Mono (software) Software using the MIT license {{Science-software-stub

Overview

References

Further reading

External links