Формальные методы анализа программ и систем: магистратура в вузах Новосибирска

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

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

Основными направлениями формальных методов, рассматриваемых в данном профиле, являются:

• Спецификация, формализация требований, онтологическое моделирование программного обеспечения и систем, что ускоряет этап их проектирования и снижает риски неопределенности и недопонимания между заказчиками и исполнителями, а также приоткрывает путь к автоматическому и/или автоматизированному доказуемо корректному синтезу программ и систем.
• Формальная семантика программ, а также методы ее аппроксимации, которые являются базой статического семантического анализа программ, результаты которого используются для их оптимизации, поиска ошибок, верификации свойств и т.д. В частности, наблюдается разрыв между прогрессом в архитектурах вычислительных систем и способностью трансляторов производить код (например, для параллельных вычислений), в полной мере использующий все возможности для высокопроизводительных вычислений. Причина этого – сложные семантические проблемы, которые приходится решать при программировании такого рода систем.
• Верификация программ и систем, т.е. доказательное подтверждение соответствия полученной реализации исходной спецификации. Это свойство ожидаемо для любого программного обеспечения, однако оно оказывается критически важным для управляющих систем реального времени, высоконадежных и устойчивых к отказам систем, разнообразных систем, связанных с обеспечением безопасности. Для решения этих задач используются сложные логические и комбинаторные методы, ведущие при реализации к нетривиальной алгоритмике.

Профессиональные дисциплины:

• Формальные методы в программной инженерии
• Методы верификации моделей программ и систем: основы
• Методы трансляции и компиляции
• Общая теория сложности
• Денотационные семантики
• Математические методы анализа данных
• Методы дедуктивной верификации программ
• Методы верификации моделей для классов программ и систем
• Функциональное программирование
• Приближенные алгоритмы
• Прикладная логика
• Универсальная алгебра
• Управление проектами
• Методы разработки формальных семантик языков программирования
• Методы проверки выполнимости булевых формул
• Параллельное программирование
• Дополнительные главы теории информации / Искусственный интеллект
• Прикладной статистический анализ
• Машинное обучение
• Автоматизированное доказательство теорем
• Основы методов проверки выполнимости формул в теориях.