Z3

Формальная верификация · SMT-решатель от Microsoft Research

создано 25 октября 2026 г. · обновлено 25 октября 2026 г.

Самый известный SMT-решатель: программа подбирает значения под заданные условия. Например, на условия «x плюс y равно десяти, x минус y равно двум» она отвечает «x равен шести, y равен четырём» или доказывает, что решений нет. Apalache отдаёт Z3 условия, полученные из модели, и по ответу строит цепочку шагов до нарушения правила.

Источник: Z3 — репозиторий на GitHub

Весь глоссарий