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 cl ...

). 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, 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 forever. Alan Turing proved in 1936 that a g ...

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 ...

, 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 GitHub, Inc. () is an Internet hosting service for software development and version control using Git. It provides the distributed version control of Git plus access control, bug tracking, software feature requests, task management, continuous ...

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