Формальные методы

У Microsoft Research есть целые исследования на эту тему. Ими занимается, если не ощибаюсь, Гуревич. Есть верификатор, написанный для C#.

Все что знаю.

Ах да, работает оно по типу контрактного программирования. То есть к C# добавлены новые конструкции. Для верификации исходный код компилируется специальным компилятором, который на эти новые конструкии и смотрит.

Этот компилятор генерирует промежуточный файл, который отдает движку доказательства теорем.

Boogie называется? Или это про Spec#? Это все, что у меня нагуглилось сходу.

Spec# вроде...

На моей прошлой работе использовали TLA(temporal logic) для верификации модели распределенной системы. Еще пытались использовать Frama C - но не хватило навыков. Сам изучал Coq, в частности для верификации интерпретатора.

а в инете много вобще находил отчетов о практических применениях.

А можешь в двух словах рассказать что за распределенная система и какого типа проблемы решали с помощью TLA?

делали model checking для проверки возможности возникновения дедлока(то что слышал из рассказов - сам этим не занимался).

Гуглим по теме: Ada, Spark. Spark - это подмножество языка Ada плюс доп. конструкции в комментах, описывающие входные-выходные параметры и еще что-то там. Не все языки программирования пригодны для подобного анализа кода. Например, C++ не подходит.

Смотрю, прикольно. Надо для хаскеля расширения посмотреть.

Кстати, а есть реальный опыт работы c этим языком? Просто в гугле куча всего подобного по данной тематике, но оно в основном вызывает впечатление дохлятины. Хочется зяться за что-нибудь живое.