Средства и методы разработки

[Satisfiability modulo theories, SMT, задача выполнимости формул в теориях] Мощнейший математический аппарат для формальной верификации ПО (в том числе). https://ru.wikipedia.org/wiki/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B2%D1%8B%D0%BF%D0%BE%D0%BB%D0%BD%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D0%B8_%D0%B1%D1%83%D0%BB%D0%B5%D0%B2%D1%8B%D1%85_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB
https://ru.wikipedia.org/wiki/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B2%D1%8B%D0%BF%D0%BE%D0%BB%D0%BD%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D0%B8_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB_%D0%B2_%D1%82%D0%B5%D0%BE%D1%80%D0%B8%D1%8F%D1%85
Есть классическая Зада́ча выполни́мости бу́левых фо́рмул (SAT) -> Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций. Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной. В SMP народ расширил теорию до небулевых формул, чем сильно повысил компактность описания реальных задач. Также создана целая куча решателей этих формул и способы формального описания формул.