T2 Temporal Prover
Script error: No such module "Infobox".Template:Template other Script error: No such module "Check for unknown parameters".Script error: No such module "Check for conflicting parameters". Script error: No such module "Portal". 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
<templatestyles src="Reflist/styles.css" />
Script error: No such module "Check for unknown parameters".
Further reading
- Script error: No such module "Citation/CS1".
External links
- T2 Temporal Logic Prover on GitHub
- T2: Temporal Property Verification publication at Microsoft Research
- Template:Webarchive
Template:Microsoft FOSS Script error: No such module "Navbox".