Формальная проверка корректности программ

Данное научное направление связано с исследованиями в области формального обоснования корректности поведения и анализа свойств программных систем. Руководит исследованиями доцент кафедры Математической кибернетики к.ф.-м.н. Владимир Анатольевич Захаров. Деятельность лаборатории исторически связана с моделированием распределённых вычислительных систем, поэтому основные результаты группы получены для следующих задач: проверки свойств поведения распределённых систем и распределённых алгоритмов, спецификации поведения распределённых систем, сравнения поведения различных систем.

Основные направления исследований группы непосредственно связаны с разработкой алгоритмов в рамках метода верификации моделей (Model Checking). Среди направлений можно выделить следующие:

Участники группы участвовали в проектах лаборатории и международных проектах:

  • Международный проект DrTesy.
  • Международный проект INTAS "Practical Formal Verification Using Automated Reasoning and Model Checking".
  • Проект "Верификация бортового ПО гражданского самолёта в соответствии с DO-178B" совместно с Гражданскими Самолётами Сухого.
  • НИР ФЦП КАДРЫ "Создание прототипа интегрированной среды и методов комплексного анализа функционирования распределённых вычислительных систем реального времени (РВС РВ)".
Password: