T2 Temporal Prover

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

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# R Open 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 Visual Studio Code 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

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

• v
• t
• e

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

• v
• t
• e