CINXE.COM
T2 Temporal Prover - Wikipedia
<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>T2 Temporal Prover - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"d8991a88-0d11-48d8-b7eb-39af25e5275b","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"T2_Temporal_Prover","wgTitle":"T2 Temporal Prover","wgCurRevisionId":1177912155,"wgRevisionId":1177912155,"wgArticleId":14627105,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Webarchive template wayback links","All stub articles","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"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"T2_Temporal_Prover","wgRelevantArticleId":14627105,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable" :true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":3000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q6840235","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled": false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init", "ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.quicksurveys.init","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="T2 Temporal Prover - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/T2_Temporal_Prover"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=T2_Temporal_Prover&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/T2_Temporal_Prover"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-T2_Temporal_Prover rootpage-T2_Temporal_Prover skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=T2+Temporal+Prover" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=T2+Temporal+Prover" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=T2+Temporal+Prover" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=T2+Temporal+Prover" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"><!-- CentralNotice --></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-Overview" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Overview"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Overview</span> </div> </a> <ul id="toc-Overview-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Further_reading" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Further_reading"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Further reading</span> </div> </a> <ul id="toc-Further_reading-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-External_links" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#External_links"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>External links</span> </div> </a> <ul id="toc-External_links-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">T2 Temporal Prover</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="This article exist only in this language. Add the article for other languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-0" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">Add languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> <div class="after-portlet after-portlet-lang"><span class="uls-after-portlet-link"></span><span class="wb-langlinks-add wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q6840235#sitelinks-wikipedia" title="Add interlanguage links" class="wbc-editpage">Add links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/T2_Temporal_Prover" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:T2_Temporal_Prover" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/T2_Temporal_Prover"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/T2_Temporal_Prover"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/T2_Temporal_Prover" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/T2_Temporal_Prover" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages" title="A list of all special pages [q]" accesskey="q"><span>Special pages</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&oldid=1177912155" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=T2_Temporal_Prover&id=1177912155&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FT2_Temporal_Prover"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FT2_Temporal_Prover"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=T2_Temporal_Prover&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=T2_Temporal_Prover&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q6840235" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><style data-mw-deduplicate="TemplateStyles:r1257001546">.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme) div:not(.notheme){background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table tr{display:table-row!important}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}</style><table class="infobox vevent"><caption class="infobox-title summary">T2 Temporal Prover</caption><tbody><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Programmer" title="Programmer">Original author(s)</a></th><td class="infobox-data"><a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Programmer" title="Programmer">Developer(s)</a></th><td class="infobox-data"><a href="/wiki/Microsoft" title="Microsoft">Microsoft</a></td></tr><tr style="display: none;"><td colspan="2" class="infobox-full-data"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1257001546"></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_release_life_cycle" title="Software release life cycle">Stable release</a></th><td class="infobox-data"><div style="margin:0px;">CADE_2017 / May 30, 2017<span class="noprint">; 7 years ago</span><span style="display:none"> (<span class="bday dtstart published updated">2017-05-30</span>)</span></div></td></tr><tr style="display:none"><td colspan="2"> </td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Repository_(version_control)" title="Repository (version control)">Repository</a></th><td class="infobox-data"><span class="url"><a rel="nofollow" class="external text" href="https://github.com/mmjb/T2">github<wbr />.com<wbr />/mmjb<wbr />/T2</a></span></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;">Written in</th><td class="infobox-data"><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Operating_system" title="Operating system">Operating system</a></th><td class="infobox-data"><a href="/wiki/Microsoft_Windows" title="Microsoft Windows">Windows</a>, <a href="/wiki/Linux" title="Linux">Linux</a> (<a href="/wiki/Debian" title="Debian">Debian</a>, <a href="/wiki/Ubuntu" title="Ubuntu">Ubuntu</a>), <a href="/wiki/MacOS" title="MacOS">macOS</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Computing_platform" title="Computing platform">Platform</a></th><td class="infobox-data"><a href="/wiki/.NET_Framework" title=".NET Framework">.NET Framework</a>, <a href="/wiki/Mono_(software)" title="Mono (software)">Mono</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_categories#Categorization_approaches" title="Software categories">Type</a></th><td class="infobox-data"><a href="/wiki/Code_analysis" class="mw-redirect" title="Code analysis">Program analyzer</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_license" title="Software license">License</a></th><td class="infobox-data"><a href="/wiki/MIT_License" title="MIT License">MIT License</a></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;">Website</th><td class="infobox-data"><span class="url"><a rel="nofollow" class="external text" href="https://www.microsoft.com/en-us/research/publication/t2-temporal-property-verification/">www<wbr />.microsoft<wbr />.com<wbr />/en-us<wbr />/research<wbr />/publication<wbr />/t2-temporal-property-verification<wbr />/</a></span></td></tr></tbody></table> <p><b>T2 Temporal Prover</b> is an automated <a href="/wiki/Code_analysis" class="mw-redirect" title="Code analysis">program analyzer</a> developed in the <i>Terminator</i> research project at <a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a>. </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=T2_Temporal_Prover&action=edit&section=1" title="Edit section: Overview"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>T2 aims to find whether a program can run infinitely (called a <a href="/wiki/Termination_analysis" title="Termination analysis">termination analysis</a>). 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 <a href="/wiki/Halting_problem" title="Halting problem">halting problem</a> for particular cases, since the general problem is <a href="/wiki/Undecidable_problem" title="Undecidable problem">undecidable</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> It provides a solution which is <a href="/wiki/Soundness" title="Soundness">sound</a>, meaning that when it states that a program does always terminate, the result is dependable. </p><p>The source code is licensed under <a href="/wiki/MIT_License" title="MIT License">MIT License</a> and hosted on <a href="/wiki/GitHub" title="GitHub">GitHub</a>.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> </p> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=T2_Temporal_Prover&action=edit&section=2" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFRob_Knies" class="citation web cs1">Rob Knies. <a rel="nofollow" class="external text" href="http://research.microsoft.com/en-us/news/features/terminator.aspx">"Terminator Tackles an Impossible Task"</a><span class="reference-accessdate">. Retrieved <span class="nowrap">2010-05-25</span></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=unknown&rft.btitle=Terminator+Tackles+an+Impossible+Task&rft.au=Rob+Knies&rft_id=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fnews%2Ffeatures%2Fterminator.aspx&rfr_id=info%3Asid%2Fen.wikipedia.org%3AT2+Temporal+Prover" class="Z3988"></span></span> </li> <li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://github.com/mmjb/T2">"GitHub - mmjb/T2: T2 Temporal Prover"</a>. December 4, 2019 – via GitHub.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=unknown&rft.btitle=GitHub+-+mmjb%2FT2%3A+T2+Temporal+Prover&rft.date=2019-12-04&rft_id=https%3A%2F%2Fgithub.com%2Fmmjb%2FT2&rfr_id=info%3Asid%2Fen.wikipedia.org%3AT2+Temporal+Prover" class="Z3988"></span></span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=T2_Temporal_Prover&action=edit&section=3" title="Edit section: Further reading"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFMarc_BrockschmidtByron_CookSamin_IshtiaqHeidy_Khlaaf2016" class="citation journal cs1">Marc Brockschmidt; Byron Cook; Samin Ishtiaq; Heidy Khlaaf; Nir Piterman (2016). "T2: Temporal Property Verification". <i>Proceedings of TACAS'16</i>. <a href="/wiki/Springer_Publishing" title="Springer Publishing">Springer</a>. <a href="/wiki/ArXiv_(identifier)" class="mw-redirect" title="ArXiv (identifier)">arXiv</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://arxiv.org/abs/1512.08689">1512.08689</a></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=Proceedings+of+TACAS%2716&rft.atitle=T2%3A+Temporal+Property+Verification&rft.date=2016&rft_id=info%3Aarxiv%2F1512.08689&rft.au=Marc+Brockschmidt&rft.au=Byron+Cook&rft.au=Samin+Ishtiaq&rft.au=Heidy+Khlaaf&rft.au=Nir+Piterman&rfr_id=info%3Asid%2Fen.wikipedia.org%3AT2+Temporal+Prover" class="Z3988"></span></li></ul> <div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=T2_Temporal_Prover&action=edit&section=4" title="Edit section: External links"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a rel="nofollow" class="external text" href="https://github.com/mmjb/T2/">T2 Temporal Logic Prover</a> on <a href="/wiki/GitHub" title="GitHub">GitHub</a></li> <li><a rel="nofollow" class="external text" href="https://www.microsoft.com/en-us/research/publication/t2-temporal-property-verification/">T2: Temporal Property Verification publication</a> at Microsoft Research</li> <li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20131004092144/http://research.microsoft.com/en-us/um/cambridge/projects/terminator/">Terminator Research Project</a> at the <a href="/wiki/Wayback_Machine" title="Wayback Machine">Wayback Machine</a> (archived October 4, 2013)</li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_free_and_open-source_software_(FOSS)" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_FOSS" title="Template:Microsoft FOSS"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_FOSS" title="Template talk:Microsoft FOSS"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_FOSS" title="Special:EditPage/Template:Microsoft FOSS"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_free_and_open-source_software_(FOSS)" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft" title="Microsoft">Microsoft</a> <a href="/wiki/Free_and_open-source_software" title="Free and open-source software">free and open-source software (FOSS)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Overview</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_and_open_source" title="Microsoft and open source">Microsoft and open source</a></li> <li><a href="/wiki/Shared_Source_Initiative" title="Shared Source Initiative">Shared Source Initiative</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Applications</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/3D_Movie_Maker" title="3D Movie Maker">3D Movie Maker</a></li> <li><a href="/wiki/Atom_(text_editor)" title="Atom (text editor)">Atom</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Family.Show" title="Family.Show">Family.Show</a></li> <li><a href="/wiki/File_Manager_(Windows)" class="mw-redirect" title="File Manager (Windows)">File Manager</a></li> <li><a href="/wiki/Open_Live_Writer" title="Open Live Writer">Open Live Writer</a></li> <li><a href="/wiki/Microsoft_PowerToys" title="Microsoft PowerToys">Microsoft PowerToys</a></li> <li><a href="/wiki/Windows_Terminal" title="Windows Terminal">Terminal</a></li> <li><a href="/wiki/Windows_Calculator" title="Windows Calculator">Windows Calculator</a></li> <li><a href="/wiki/Windows_Console" title="Windows Console">Windows Console</a></li> <li><a href="/wiki/Windows_Package_Manager" title="Windows Package Manager">Windows Package Manager</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/XML_Notepad" title="XML Notepad">XML Notepad</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Video games</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Programming<br />languages</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/Dafny" title="Dafny">Dafny</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/GW-BASIC" title="GW-BASIC">GW-BASIC</a></li> <li><a href="/wiki/IronPython" title="IronPython">IronPython</a></li> <li><a href="/wiki/IronRuby" title="IronRuby">IronRuby</a></li> <li><a href="/wiki/Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Microsoft_Power_Fx" title="Microsoft Power Fx">Power Fx</a></li> <li><a href="/wiki/PowerShell" title="PowerShell">PowerShell</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Q_Sharp" title="Q Sharp">Q#</a></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic Online</a></li> <li><a href="/wiki/TypeScript" title="TypeScript">TypeScript</a></li> <li><a href="/wiki/Visual_Basic_.NET" class="mw-redirect" title="Visual Basic .NET">Visual Basic</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Frameworks,<br />development tools</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET" title=".NET">.NET</a></li> <li><a href="/wiki/.NET_Framework" title=".NET Framework">.NET Framework</a></li> <li><a href="/wiki/.NET_Gadgeteer" title=".NET Gadgeteer">.NET Gadgeteer</a></li> <li><a href="/wiki/.NET_MAUI" class="mw-redirect" title=".NET MAUI">.NET MAUI</a></li> <li><a href="/wiki/.NET_Micro_Framework" title=".NET Micro Framework">.NET Micro Framework</a></li> <li><a href="/wiki/AirSim" title="AirSim">AirSim</a></li> <li><a href="/wiki/ASP.NET" title="ASP.NET">ASP.NET</a></li> <li><a href="/wiki/ASP.NET_AJAX" title="ASP.NET AJAX">ASP.NET AJAX</a></li> <li><a href="/wiki/ASP.NET_Core" title="ASP.NET Core">ASP.NET Core</a></li> <li><a href="/wiki/ASP.NET_MVC" title="ASP.NET MVC">ASP.NET MVC</a></li> <li><a href="/wiki/ASP.NET_Razor" title="ASP.NET Razor">ASP.NET Razor</a></li> <li><a href="/wiki/ASP.NET_Web_Forms" title="ASP.NET Web Forms">ASP.NET Web Forms</a></li> <li><a href="/wiki/Avalonia_(software_framework)" title="Avalonia (software framework)">Avalonia</a></li> <li><a href="/wiki/Babylon.js" title="Babylon.js">Babylon.js</a></li> <li><a href="/wiki/BitFunnel" title="BitFunnel">BitFunnel</a></li> <li><a href="/wiki/Blazor" title="Blazor">Blazor</a></li> <li><a href="/wiki/C%2B%2B/WinRT" title="C++/WinRT">C++/WinRT</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">CCF</a></li> <li><a href="/wiki/Chakra_(JavaScript_engine)" title="Chakra (JavaScript engine)">ChakraCore</a></li> <li><a href="/wiki/CLR_Profiler" title="CLR Profiler">CLR Profiler</a></li> <li><a href="/wiki/Dapr" title="Dapr">Dapr</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/DiskSpd" title="DiskSpd">DiskSpd</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Dynamic_Language_Runtime" title="Dynamic Language Runtime">Dynamic Language Runtime</a></li> <li><a href="/wiki/EBPF_on_Windows" class="mw-redirect" title="EBPF on Windows">eBPF on Windows</a></li> <li><a href="/wiki/Electron_(software_framework)" title="Electron (software framework)">Electron</a></li> <li><a href="/wiki/Entity_Framework" title="Entity Framework">Entity Framework</a></li> <li><a href="/wiki/Fluent_Design_System" title="Fluent Design System">Fluent Design System</a></li> <li><a href="/wiki/Fluid_Framework" title="Fluid Framework">Fluid Framework</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/Managed_Extensibility_Framework" title="Managed Extensibility Framework">Managed Extensibility Framework</a></li> <li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Microsoft Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_C%2B%2B_Standard_Library" class="mw-redirect" title="Microsoft C++ Standard Library">Microsoft C++ Standard Library</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Microsoft Cognitive Toolkit</a></li> <li><a href="/wiki/Metro_(design_language)" title="Metro (design language)">Microsoft Design Language</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Microsoft Detours</a></li> <li><a href="/wiki/Microsoft_Enterprise_Library" title="Microsoft Enterprise Library">Microsoft Enterprise Library</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">Microsoft SEAL</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/Mixed_Reality_Toolkit" title="Mixed Reality Toolkit">Mixed Reality Toolkit</a></li> <li><a href="/wiki/ML.NET" title="ML.NET">ML.NET</a></li> <li><a href="/wiki/Mod_mono" title="Mod mono">mod_mono</a></li> <li><a href="/wiki/Mono_(software)" title="Mono (software)">Mono</a></li> <li><a href="/wiki/MonoDevelop" title="MonoDevelop">MonoDevelop</a></li> <li><a href="/wiki/MSBuild" title="MSBuild">MSBuild</a></li> <li><a href="/wiki/MsQuic" title="MsQuic">MsQuic</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/Npm" title="Npm">npm</a></li> <li><a href="/wiki/NuGet" title="NuGet">NuGet</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/Open_Management_Infrastructure" title="Open Management Infrastructure">Open Management Infrastructure</a></li> <li><a href="/wiki/Open_Neural_Network_Exchange" title="Open Neural Network Exchange">Open Neural Network Exchange</a></li> <li><a href="/wiki/Open_Service_Mesh" title="Open Service Mesh">Open Service Mesh</a></li> <li><a href="/wiki/Open_XML_SDK" class="mw-redirect" title="Open XML SDK">Open XML SDK</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li> <li><a href="/wiki/Playwright_(software)" title="Playwright (software)">Playwright</a></li> <li><a href="/wiki/ProcDump" title="ProcDump">ProcDump</a></li> <li><a href="/wiki/Process_Monitor" title="Process Monitor">ProcMon</a></li> <li><a href="/wiki/Python_Tools_for_Visual_Studio" title="Python Tools for Visual Studio">Python Tools for Visual Studio</a></li> <li><a href="/wiki/R_Tools_for_Visual_Studio" title="R Tools for Visual Studio">R Tools for Visual Studio</a></li> <li><a href="/wiki/RecursiveExtractor" class="mw-redirect" title="RecursiveExtractor">RecursiveExtractor</a></li> <li><a href="/wiki/Roslyn_(compiler)" title="Roslyn (compiler)">Roslyn</a></li> <li><a href="/wiki/Sandcastle_(software)" title="Sandcastle (software)">Sandcastle</a></li> <li><a href="/wiki/SignalR" title="SignalR">SignalR</a></li> <li><a href="/wiki/StyleCop" title="StyleCop">StyleCop</a></li> <li><a href="/wiki/SVNBridge" title="SVNBridge">SVNBridge</a></li> <li><a class="mw-selflink selflink">T2 Temporal Prover</a></li> <li><a href="/wiki/Text_Template_Transformation_Toolkit" title="Text Template Transformation Toolkit">Text Template Transformation Toolkit</a></li> <li><a href="/wiki/TLA%2B_Toolbox" class="mw-redirect" title="TLA+ Toolbox">TLA+ Toolbox</a></li> <li><a href="/wiki/U-Prove" title="U-Prove">U-Prove</a></li> <li><a href="/wiki/Vcpkg" title="Vcpkg">vcpkg</a></li> <li><a href="/wiki/Virtual_File_System_for_Git" title="Virtual File System for Git">Virtual File System for Git</a></li> <li><a href="/wiki/Voldemort_(distributed_data_store)" title="Voldemort (distributed data store)">Voldemort</a></li> <li><a href="/wiki/VoTT" title="VoTT">VoTT</a></li> <li><a href="/wiki/Vowpal_Wabbit" title="Vowpal Wabbit">Vowpal Wabbit</a></li> <li><a href="/wiki/Windows_App_SDK" title="Windows App SDK">Windows App SDK</a></li> <li><a href="/wiki/Windows_Communication_Foundation" title="Windows Communication Foundation">Windows Communication Foundation</a></li> <li><a href="/wiki/Windows_Driver_Frameworks" title="Windows Driver Frameworks">Windows Driver Frameworks</a> <ul><li><a href="/wiki/Kernel-Mode_Driver_Framework" title="Kernel-Mode Driver Framework">KMDF</a></li> <li><a href="/wiki/User-Mode_Driver_Framework" title="User-Mode Driver Framework">UMDF</a></li></ul></li> <li><a href="/wiki/Windows_Forms" title="Windows Forms">Windows Forms</a></li> <li><a href="/wiki/Windows_Presentation_Foundation" title="Windows Presentation Foundation">Windows Presentation Foundation</a></li> <li><a href="/wiki/Windows_Template_Library" title="Windows Template Library">Windows Template Library</a></li> <li><a href="/wiki/Windows_UI_Library" title="Windows UI Library">Windows UI Library</a></li> <li><a href="/wiki/WinJS" title="WinJS">WinJS</a></li> <li><a href="/wiki/WinObjC" class="mw-redirect" title="WinObjC">WinObjC</a></li> <li><a href="/wiki/WiX" title="WiX">WiX</a></li> <li><a href="/wiki/XDP_for_Windows" class="mw-redirect" title="XDP for Windows">XDP for Windows</a></li> <li><a href="/wiki/XSP_(software)" title="XSP (software)">XSP</a></li> <li><a href="/wiki/XUnit.net" title="XUnit.net">xUnit.net</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Operating systems</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/MS-DOS" title="MS-DOS">MS-DOS</a> (v1.25, v2.0 & v4.0)</li> <li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/SONiC_(operating_system)" title="SONiC (operating system)">SONiC</a></li> <li><a href="/wiki/Azure_Linux" title="Azure Linux">Azure Linux</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ChronoZoom" title="ChronoZoom">ChronoZoom</a></li> <li><a href="/wiki/Extensible_Storage_Engine" title="Extensible Storage Engine">Extensible Storage Engine</a></li> <li><a href="/wiki/FlexWiki" class="mw-redirect" title="FlexWiki">FlexWiki</a></li> <li><a href="/wiki/FourQ" title="FourQ">FourQ</a></li> <li><a href="/wiki/Gollum_(software)" title="Gollum (software)">Gollum</a></li> <li><a href="/wiki/Project_Mu" class="mw-redirect" title="Project Mu">Project Mu</a></li> <li><a href="/wiki/ReactiveX" title="ReactiveX">ReactiveX</a></li> <li><a href="/wiki/SILK" title="SILK">SILK</a></li> <li><a href="/wiki/TLAPS" class="mw-redirect" title="TLAPS">TLAPS</a></li> <li><a href="/wiki/TPM_2.0_Reference_Implementation" class="mw-redirect" title="TPM 2.0 Reference Implementation">TPM 2.0 Reference Implementation</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Open-source_license" title="Open-source license">Licenses</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Public_License" class="mw-redirect" title="Microsoft Public License">Microsoft Public License</a></li> <li><a href="/wiki/Microsoft_Reciprocal_License" class="mw-redirect" title="Microsoft Reciprocal License">Microsoft Reciprocal License</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Forge_(software)" title="Forge (software)">Forges</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/CodePlex" title="CodePlex">CodePlex</a></li> <li><a href="/wiki/GitHub" title="GitHub">GitHub</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET_Foundation" title=".NET Foundation">.NET Foundation</a></li> <li><a href="/wiki/F_Sharp_Software_Foundation" title="F Sharp Software Foundation">F# Software Foundation</a></li> <li><a href="/wiki/Microsoft_Open_Specification_Promise" title="Microsoft Open Specification Promise">Microsoft Open Specification Promise</a></li> <li><a href="/wiki/Open_Letter_to_Hobbyists" class="mw-redirect" title="Open Letter to Hobbyists">Open Letter to Hobbyists</a></li> <li><a href="/wiki/Open_Source_Security_Foundation" title="Open Source Security Foundation">Open Source Security Foundation</a></li> <li><a href="/wiki/Outercurve_Foundation" title="Outercurve Foundation">Outercurve Foundation</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Category</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_Research_(MSR)" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_Research" title="Template:Microsoft Research"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_Research" title="Template talk:Microsoft Research"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_Research" title="Special:EditPage/Template:Microsoft Research"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_Research_(MSR)" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research (MSR)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Main<br />projects</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Languages, compilers</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bartok_(compiler)" title="Bartok (compiler)">Bartok</a></li> <li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C%CF%89" class="mw-redirect" title="Cω">Cω</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Microsoft_Phoenix" title="Microsoft Phoenix">Phoenix</a></li> <li><a href="/wiki/Polyphonic_C_Sharp" class="mw-redirect" title="Polyphonic C Sharp">Polyphonic C#</a></li> <li><a href="/wiki/SecPAL" title="SecPAL">SecPAL</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Distributed_computing" title="Distributed computing">Distributed</a>–<a href="/wiki/Grid_computing" title="Grid computing">grid computing</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/BitVault" title="BitVault">BitVault</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">Confidential Consortium Framework</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Internet" title="Internet">Internet</a>, <a href="/wiki/Computer_network" title="Computer network">networking</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/AjaxView" title="AjaxView">AjaxView</a></li> <li><a href="/wiki/Avalanche_(P2P)" title="Avalanche (P2P)">Avalanche</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Gazelle_(web_browser)" title="Gazelle (web browser)">Gazelle</a></li> <li><a href="/wiki/HoneyMonkey" title="HoneyMonkey">HoneyMonkey</a></li> <li><a href="/wiki/Penny_Black_(research_project)" title="Penny Black (research project)">Penny Black</a></li> <li><a href="/wiki/Wallop" title="Wallop">Wallop</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other projects</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Cognitive Toolkit</a></li> <li><a href="/wiki/Project_Digits" title="Project Digits">Digits</a></li> <li><a href="/wiki/Microsoft_Holoportation" title="Microsoft Holoportation">Holoportation</a></li> <li><a href="/wiki/IllumiRoom" title="IllumiRoom">IllumiRoom</a></li> <li><a href="/wiki/Image_Composite_Editor" title="Image Composite Editor">Image Composite Editor</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/LiveStation" title="LiveStation">LiveStation</a></li> <li><a href="/wiki/MyLifeBits" title="MyLifeBits">MyLifeBits</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/NodeXL" title="NodeXL">NodeXL</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/PhotoDNA" title="PhotoDNA">PhotoDNA</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">SEAL</a></li> <li><a href="/wiki/SLAM_project" title="SLAM project">SLAM</a></li> <li><a class="mw-selflink selflink">T2 Temporal Prover</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Operating_system" title="Operating system">Operating systems</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/HomeOS" title="HomeOS">HomeOS</a></li> <li><a href="/wiki/Midori_(operating_system)" title="Midori (operating system)">Midori</a></li> <li><a href="/wiki/Singularity_(operating_system)" title="Singularity (operating system)">Singularity</a></li> <li><a href="/wiki/Verve_(operating_system)" title="Verve (operating system)">Verve</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/API" title="API">APIs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Accelerator_(library)" title="Accelerator (library)">Accelerator</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Joins_(concurrency_library)" title="Joins (concurrency library)">Joins</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/SXM_(transactional_memory)" title="SXM (transactional memory)">SXM</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Launched as products</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/Microsoft_Comic_Chat" title="Microsoft Comic Chat">Comic Chat</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Detours</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/Windows_Desktop_Gadgets" title="Windows Desktop Gadgets">Sideshow</a></li> <li><a href="/wiki/Microsoft_PixelSense" title="Microsoft PixelSense">PixelSense</a> (<a href="/wiki/TouchLight" title="TouchLight">TouchLight</a>)</li> <li><a href="/wiki/Microsoft_SenseCam" title="Microsoft SenseCam">SenseCam</a></li> <li><a href="/wiki/ClearType" title="ClearType">ClearType</a></li> <li><a href="/wiki/Group_Shot" title="Group Shot">Group Shot</a></li> <li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li> <li><a href="/wiki/TrueSkill" title="TrueSkill">TrueSkill</a></li> <li><a href="/wiki/Microsoft_Songsmith" class="mw-redirect" title="Microsoft Songsmith">Songsmith</a></li> <li><a href="/wiki/Xbox" title="Xbox">Xbox</a> <ul><li><a href="/wiki/Kinect" title="Kinect">Kinect</a></li></ul></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">MSR Labs<br />applied<br />research</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_Live_Labs" title="Microsoft Live Labs">Live Labs</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Current</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Pivot" title="Microsoft Live Labs Pivot">Pivot</a></li> <li><a href="/wiki/Seadragon_Software" title="Seadragon Software">Seadragon</a> <ul><li><a href="/wiki/Deep_Zoom" title="Deep Zoom">Deep Zoom</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Discontinued</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Deepfish" title="Microsoft Live Labs Deepfish">Deepfish</a></li> <li><a href="/wiki/Microsoft_Live_Labs_Listas" title="Microsoft Live Labs Listas">Listas</a></li> <li><a href="/wiki/Live_Clipboard" title="Live Clipboard">Live Clipboard</a></li> <li><a href="/wiki/Photosynth" title="Photosynth">Photosynth</a></li> <li><a href="/wiki/Microsoft_Live_Labs_Volta" title="Microsoft Live Labs Volta">Volta</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_FUSE_Labs" title="Microsoft FUSE Labs">FUSE Labs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Docs.com" title="Docs.com">Docs.com</a></li> <li><a href="/wiki/Kodu_Game_Lab" title="Kodu Game Lab">Kodu</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other labs</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Academic_Search" title="Microsoft Academic Search">Academic Search</a></li> <li><a href="/wiki/Microsoft_adCenter_Labs" title="Microsoft adCenter Labs">adCenter Labs</a></li> <li><a href="/wiki/Microsoft_Office" title="Microsoft Office">Office Labs</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Category</a></div></td></tr></tbody></table></div> <style data-mw-deduplicate="TemplateStyles:r1012311289">.mw-parser-output .asbox{position:relative;overflow:hidden}.mw-parser-output .asbox table{background:transparent}.mw-parser-output .asbox p{margin:0}.mw-parser-output .asbox p+p{margin-top:0.25em}.mw-parser-output .asbox-body{font-style:italic}.mw-parser-output .asbox-note{font-size:smaller}.mw-parser-output .asbox .navbar{position:absolute;top:-0.75em;right:1em;display:none}</style><div role="note" class="metadata plainlinks asbox stub"><table role="presentation"><tbody><tr class="noresize"><td><span typeof="mw:File"><a href="/wiki/File:Windows_logo_-_2021.svg" class="mw-file-description"><img alt="Stub icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/8/87/Windows_logo_-_2021.svg/30px-Windows_logo_-_2021.svg.png" decoding="async" width="30" height="30" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/8/87/Windows_logo_-_2021.svg/45px-Windows_logo_-_2021.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/8/87/Windows_logo_-_2021.svg/60px-Windows_logo_-_2021.svg.png 2x" data-file-width="512" data-file-height="512" /></a></span></td><td><p class="asbox-body">This <a href="/wiki/Microsoft_Windows" title="Microsoft Windows">Microsoft Windows</a> <a href="/wiki/Software" title="Software">software</a>-related article is a <a href="/wiki/Wikipedia:Stub" title="Wikipedia:Stub">stub</a>. You can help Wikipedia by <a class="external text" href="https://en.wikipedia.org/w/index.php?title=T2_Temporal_Prover&action=edit">expanding it</a>.</p></td></tr></tbody></table><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Windows-software-stub" title="Template:Windows-software-stub"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Windows-software-stub" title="Template talk:Windows-software-stub"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Windows-software-stub" title="Special:EditPage/Template:Windows-software-stub"><abbr title="Edit this template">e</abbr></a></li></ul></div></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1012311289"><div role="note" class="metadata plainlinks asbox stub"><table role="presentation"><tbody><tr class="noresize"><td><span typeof="mw:File"><a href="/wiki/File:Science-symbol-2.svg" class="mw-file-description"><img alt="Stub icon" src="//upload.wikimedia.org/wikipedia/commons/thumb/7/75/Science-symbol-2.svg/30px-Science-symbol-2.svg.png" decoding="async" width="30" height="30" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/7/75/Science-symbol-2.svg/45px-Science-symbol-2.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/7/75/Science-symbol-2.svg/60px-Science-symbol-2.svg.png 2x" data-file-width="87" data-file-height="87" /></a></span></td><td><p class="asbox-body">This <a href="/wiki/Software" title="Software">scientific software</a> article is a <a href="/wiki/Wikipedia:Stub" title="Wikipedia:Stub">stub</a>. You can help Wikipedia by <a class="external text" href="https://en.wikipedia.org/w/index.php?title=T2_Temporal_Prover&action=edit">expanding it</a>.</p></td></tr></tbody></table><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Science-software-stub" title="Template:Science-software-stub"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Science-software-stub" title="Template talk:Science-software-stub"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Science-software-stub" title="Special:EditPage/Template:Science-software-stub"><abbr title="Edit this template">e</abbr></a></li></ul></div></div> <!-- NewPP limit report Parsed by mw‐web.eqiad.main‐5dc468848‐f96l7 Cached time: 20241124073913 Cache expiry: 2592000 Reduced expiry: false Complications: [vary‐revision‐sha1, show‐toc] CPU time usage: 0.376 seconds Real time usage: 0.473 seconds Preprocessor visited node count: 1332/1000000 Post‐expand include size: 88122/2097152 bytes Template argument size: 2489/2097152 bytes Highest expansion depth: 27/100 Expensive parser function count: 3/500 Unstrip recursion depth: 1/20 Unstrip post‐expand size: 36767/5000000 bytes Lua time usage: 0.231/10.000 seconds Lua memory usage: 4559105/52428800 bytes Number of Wikibase entities loaded: 1/400 --> <!-- Transclusion expansion time report (%,ms,calls,template) 100.00% 391.782 1 -total 38.64% 151.390 2 Template:Infobox 29.93% 117.245 1 Template:Reflist 29.89% 117.102 6 Template:Navbox 27.74% 108.686 1 Template:Infobox_software 26.52% 103.906 2 Template:Cite_web 25.62% 100.370 1 Template:Microsoft_FOSS 13.39% 52.473 1 Template:Infobox_software/simple 6.01% 23.540 1 Template:Windows-software-stub 5.58% 21.862 1 Template:Start_date_and_age --> <!-- Saved in parser cache with key enwiki:pcache:idhash:14627105-0!canonical and timestamp 20241124073913 and revision id 1177912155. Rendering was triggered because: page-view --> </div><!--esi <esi:include src="/esitest-fa8a495983347898/content" /> --><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=T2_Temporal_Prover&oldid=1177912155">https://en.wikipedia.org/w/index.php?title=T2_Temporal_Prover&oldid=1177912155</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/wiki/Category:Free_and_open-source_software" title="Category:Free and open-source software">Free and open-source software</a></li><li><a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Microsoft free software</a></li><li><a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Microsoft Research</a></li><li><a href="/wiki/Category:Software_that_uses_Mono_(software)" title="Category:Software that uses Mono (software)">Software that uses Mono (software)</a></li><li><a href="/wiki/Category:Software_using_the_MIT_license" title="Category:Software using the MIT license">Software using the MIT license</a></li><li><a href="/wiki/Category:Windows_software_stubs" title="Category:Windows software stubs">Windows software stubs</a></li><li><a href="/wiki/Category:Science_software_stubs" title="Category:Science software stubs">Science software stubs</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Webarchive_template_wayback_links" title="Category:Webarchive template wayback links">Webarchive template wayback links</a></li><li><a href="/wiki/Category:All_stub_articles" title="Category:All stub articles">All stub articles</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 30 September 2023, at 12:04<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=T2_Temporal_Prover&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-694cf4987f-s2f92","wgBackendResponseTime":135,"wgPageParseReport":{"limitreport":{"cputime":"0.376","walltime":"0.473","ppvisitednodes":{"value":1332,"limit":1000000},"postexpandincludesize":{"value":88122,"limit":2097152},"templateargumentsize":{"value":2489,"limit":2097152},"expansiondepth":{"value":27,"limit":100},"expensivefunctioncount":{"value":3,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":36767,"limit":5000000},"entityaccesscount":{"value":1,"limit":400},"timingprofile":["100.00% 391.782 1 -total"," 38.64% 151.390 2 Template:Infobox"," 29.93% 117.245 1 Template:Reflist"," 29.89% 117.102 6 Template:Navbox"," 27.74% 108.686 1 Template:Infobox_software"," 26.52% 103.906 2 Template:Cite_web"," 25.62% 100.370 1 Template:Microsoft_FOSS"," 13.39% 52.473 1 Template:Infobox_software/simple"," 6.01% 23.540 1 Template:Windows-software-stub"," 5.58% 21.862 1 Template:Start_date_and_age"]},"scribunto":{"limitreport-timeusage":{"value":"0.231","limit":"10.000"},"limitreport-memusage":{"value":4559105,"limit":52428800}},"cachereport":{"origin":"mw-web.eqiad.main-5dc468848-f96l7","timestamp":"20241124073913","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"T2 Temporal Prover","url":"https:\/\/en.wikipedia.org\/wiki\/T2_Temporal_Prover","sameAs":"http:\/\/www.wikidata.org\/entity\/Q6840235","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q6840235","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2007-12-09T10:31:32Z","dateModified":"2023-09-30T12:04:53Z","headline":"program analyzer research project"}</script> </body> </html>