Временное обеспечение T2

Временное обеспечение T2
Оригинальный автор(ы)	Microsoft Исследования
Разработчик(и)	Майкрософт
Стабильная версия	CADE_2017 / 30 мая 2017 г .; 7 лет назад
Репозиторий	github .с /ммджб /Т2
Написано в	Ф#
Операционная система	Windows , Linux ( Debian , Ubuntu ), macOS
Платформа	.NET Framework , моно
Тип	Анализатор программ
Лицензия	МОЯ лицензия
Веб-сайт	www .microsoft .с /en-нас /исследовать /публикация /t2-temporal-property-verification /

T2 Temporal Prover — автоматизированный анализатор программ, разработанный в рамках исследовательского проекта Terminator в Microsoft Research .

Обзор

T2 направлен на то, чтобы выяснить, может ли программа работать бесконечно (так называемый анализ завершения ). Он поддерживает вложенные циклы и рекурсивные функции, указатели и побочные эффекты, указатели на функции, а также параллельные программы. Как и все программы для анализа завершения, она пытается решить проблему остановки для частных случаев, поскольку общая проблема неразрешима . ^{[ 1 ]} решение Он предоставляет разумное , а это означает, что когда оно утверждает, что программа всегда завершается, результат надежен.

Исходный код лицензируется по лицензии MIT License и размещен на GitHub . ^{[ 2 ]}

Ссылки

^ Роб Книс. «Терминатор решает невыполнимую задачу» . Проверено 25 мая 2010 г.
^ «GitHub — mmjb/T2: Темпоральный проверяющий модуль T2» . 4 декабря 2019 г. – через GitHub.

Дальнейшее чтение

Марк Брокшмидт; Байрон Кук; Самин Иштиак; Хейди Клааф; Нир Питерман (2016). «T2: Проверка временной собственности». Материалы TACAS'16 . Спрингер . arXiv : 1512.08689 .