SPIN

Интересные факты о SPIN
Для доказательства корректности алгоритма редукции, то есть сохранения свойств безопасности и живости был использован доказатель теорем HOL.

Вычислительная сложность алгоритмов для доказательства свойств безопасности, таких как отсутствие дедлоков или пользовательских ассертов, линейно растёт от количества достижимых состояний, и для процессорного времени и для требуемого объёма памяти.

Для доказательства простых свойств живости, таких как отсутствие удушения или принимающих циклов (циклов, включающих принимающие состояния автомата Бюхи), требуется не больше чем квадратичное время, но требования к памяти не увеличиваются существенно.

Для доказательства свойств, выраженных формулами линейной темпоральной логики, требования по времени увеличиваются за счёт множителя, который в худшем случае сам зависит экспоненциально от количества темпоральных операторов в формуле. Требования к памяти, существенно не увеличиваются.

Все эти факты содержатся в статье G. Holzmann "The Model Checker Spin".