T2 Temporal Prover

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

• 1 Обзор
• 2 Ссылки
• 3 Дополнительная литература
• 4 Внешние ссылки

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

Исходный код под лицензией MIT License и размещен на GitHub.

• Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Хейди Хлааф, Нир Питерман (2016). «T2: Проверка временных свойств». Материалы ТАКАС'16. Springer. CS1 maint: использует параметр авторов (ссылка )

• T2 Temporal Logic Prover на GitHub
• T2: Temporal Property Verification публикация в Microsoft Research
• Terminator Research Project в Wayback Machine (архивировано 4 октября 2013 г.)