SMT-решатель
Формальная верификация · например, Z3
создано · обновлено
Программа, которая по набору условий вроде «сумма больше десяти, а счёт не отрицательный» сама находит значения, при которых все условия выполняются, или доказывает, что таких значений нет. Перебирать всё подряд ей не нужно: она рассуждает о целых классах случаев сразу. Самый известный решатель Z3 создала Microsoft Research. Движок Apalache переводит модель в такие условия и отдаёт их решателю.
Источник: Z3 — репозиторий решателя на GitHub