T2 Temporal Prover - T2 Temporal Prover
T2 Temporal Prover это автоматизированный программный анализатор разработан в Терминатор исследовательский проект в Microsoft Research.
Обзор
T2 стремится определить, может ли программа работать бесконечно (так называемая анализ прекращения ). Он поддерживает вложенные циклы и рекурсивные функции, указатели и побочные эффекты, указатели на функции, а также параллельные программы. Как и все программы для анализа завершения, он пытается решить проблема остановки для частных случаев, поскольку общая проблема неразрешимый.[1] Это решение, которое звук, что означает, что когда в нем говорится, что программа всегда завершается, результат надежен.
Исходный код находится под лицензией Лицензия MIT и размещен на GitHub.[2]
Рекомендации
- ^ Роб Knies. «Терминатор решает невыполнимую задачу». Получено 2010-05-25.
- ^ "GitHub - mmjb / T2: T2 Temporal Prover". 4 декабря 2019 г. - через GitHub.
дальнейшее чтение
- Марк Брокшмидт, Байрон Кук, Самин Иштиак, Хейди Хлааф, Нир Питерман (2016). «T2: Проверка временных свойств». Материалы TACAS'16. Springer.CS1 maint: использует параметр авторов (связь)
внешняя ссылка
- T2 Temporal Logic Prover на GitHub
- T2: публикация проверки временных свойств в Microsoft Research
- Исследовательский проект Терминатора на Wayback Machine (архивировано 4 октября 2013 г.)
Категория | Этот Майкрософт Виндоус программного обеспечения -связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |
 | Этот научное программное обеспечение статья - это заглушка. Вы можете помочь Википедии расширяя это. |