Misplaced Pages

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

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

• Marc Brockschmidt; Byron Cook; Samin Ishtiaq; Heidy Khlaaf; Nir Piterman (2016). "T2: Temporal Property Verification". Proceedings of TACAS'16. Springer. arXiv:1512.08689.

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)

v t e Microsoft free and open-source software (FOSS)
Overview	Microsoft and open source Shared Source Initiative
Software	Applications 3D Movie Maker Atom Conference XP Family.Show File Manager Open Live Writer Microsoft PowerToys Terminal Windows Calculator Windows Console Windows Package Manager WorldWide Telescope XML Notepad Video games Allegiance Programming languages Bosque C# Dafny F# F* GW-BASIC IronPython IronRuby Lean P Power Fx PowerShell Project Verona Q# Small Basic Online TypeScript Visual Basic Frameworks, development tools .NET .NET Framework .NET Gadgeteer .NET MAUI .NET Micro Framework AirSim ASP.NET ASP.NET AJAX ASP.NET Core ASP.NET MVC ASP.NET Razor ASP.NET Web Forms Avalonia Babylon.js BitFunnel Blazor C++/WinRT CCF ChakraCore CLR Profiler Dapr DeepSpeed DiskSpd Dryad Dynamic Language Runtime eBPF on Windows Electron Entity Framework Fluent Design System Fluid Framework Infer.NET LightGBM Managed Extensibility Framework Microsoft Automatic Graph Layout Microsoft C++ Standard Library Microsoft Cognitive Toolkit Microsoft Design Language Microsoft Detours Microsoft Enterprise Library Microsoft SEAL mimalloc Mixed Reality Toolkit ML.NET mod_mono Mono MonoDevelop MSBuild MsQuic Neural Network Intelligence npm NuGet OneFuzz Open Management Infrastructure Open Neural Network Exchange Open Service Mesh Open XML SDK Orleans Playwright ProcDump ProcMon Python Tools for Visual Studio R Tools for Visual Studio RecursiveExtractor Roslyn Sandcastle SignalR StyleCop SVNBridge T2 Temporal Prover Text Template Transformation Toolkit TLA+ Toolbox U-Prove vcpkg Virtual File System for Git Voldemort VoTT Vowpal Wabbit Windows App SDK Windows Communication Foundation Windows Driver Frameworks KMDF UMDF Windows Forms Windows Presentation Foundation Windows Template Library Windows UI Library WinJS WinObjC WiX XDP for Windows XSP xUnit.net Z3 Theorem Prover Operating systems MS-DOS (v1.25, v2.0 & v4.0) Barrelfish SONiC Azure Linux Other ChronoZoom Extensible Storage Engine FlexWiki FourQ Gollum Project Mu ReactiveX SILK TLAPS TPM 2.0 Reference Implementation WikiBhasha
Licenses	Microsoft Public License Microsoft Reciprocal License
Forges	CodePlex GitHub
Related	.NET Foundation F# Software Foundation Microsoft Open Specification Promise Open Letter to Hobbyists Open Source Security Foundation Outercurve Foundation
Category

v t e Microsoft Research (MSR)
Main projects	Languages, compilers Bartok Bosque Cω F* Lean P Project Verona Phoenix Polyphonic C# SecPAL Distributed–grid computing BitVault Confidential Consortium Framework DeepSpeed Orleans Internet, networking AjaxView Avalanche Conference XP Gazelle HoneyMonkey Penny Black Wallop WikiBhasha Other projects Automatic Graph Layout Cognitive Toolkit Digits Holoportation IllumiRoom Image Composite Editor Infer.NET LightGBM LiveStation MyLifeBits Neural Network Intelligence NodeXL OneFuzz PhotoDNA SEAL SLAM T2 Temporal Prover WorldWide Telescope Z3 Theorem Prover Operating systems Barrelfish HomeOS Midori Singularity Verve APIs Accelerator Dryad Joins mimalloc SXM Launched as products C# Comic Chat Detours F# Sideshow PixelSense (TouchLight) SenseCam ClearType Group Shot Allegiance TrueSkill Songsmith Xbox Kinect
MSR Labs applied research	Live Labs Current Pivot Seadragon Deep Zoom Discontinued Deepfish Listas Live Clipboard Photosynth Volta FUSE Labs Docs.com Kodu Other labs Academic Search adCenter Labs Office Labs
Category

This Microsoft Windows software-related article is a stub. You can help Misplaced Pages by expanding it.

• v
• t
• e

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

• v
• t
• e

• Free and open-source software
• Microsoft free software
• Microsoft Research
• Software that uses Mono (software)
• Software using the MIT license
• Windows software stubs
• Science software stubs