Apalache
Формальная верификация · символьная проверка моделей
создано · обновлено
Программа, которая проверяет модели на TLA+ и на Quint. Она переводит их в набор условий и отдаёт SMT-решателю, например Z3: тот рассуждает сразу обо всех исполнениях до заданной длины. Выдаёт цепочку шагов, где правило нарушается.
Источник: apalache-mc.org — сайт Apalache
Где встречается · 3
- Как найти состояние гонки (race condition) в коде · Спеки и контекст
- Чем model checking отличается от тестов · Спеки и контекст
- Какой язык формальной верификации выбрать · Спеки и контекст