О ЛАБОРАТОРИИ
Лаборатория математического моделирования, логики, формальных методов доказательства.
Лаборатория исследует методы математического моделирования и формальной верификации программных, киберфизических и защищенных систем. Мы формализуем требования к надежности и безопасности, строим модели поведения систем и проверяем выполнение критических свойств с помощью доказательных методов и инструментов формальной математики.
Формальная верификация программных и киберсистем
Математическое доказательство того, что рассматриваемая система (киберсистема) полностью соответствует заданным формальным требованиям/спецификации.
01
Математическое моделирование киберсистем
Создание и анализ математической модели распределенной киберфизической системы, процесса, ПО, СЗИ для изучения их поведения, прогнозирования наблюдаемых результатов и последующего принятия решения.
02
Теория доказательств. Логика
Раздел логики, исследующий методы построения математических доказательств, а также их доказуемость.
03
Гомотопическая теория типов
Математическая теория, рассматривающая типы как геометрические объекты и использующая методы алгебраической топологии для формального описания и доказательства математических утверждений.
04
Функциональные языки и формальная семантика
Стиль создания кода, где программы строятся исключительно на основе математических функций и неизменяемых данных.
05
Направления исследований
УСЛУГИ БИЗНЕСУ
-
Формальная верификация критического ПО и киберсистемЭкспертиза корректности работы киберфизических систем, программных алгоритмов и инженерных решений с оценкой корректности, устойчивости и соответствия заданным требованиям (спецификации/инвариантам), построение контрпрримеров. -
Оптимизация и надежность алгоритмовРазработка алгоритмов оптимизации затрат, ресурсов, производственных планов и логистических цепочек с использованием современных математических методов. -
Математическое и имитационное моделирование процессов и системРазработка цифровых моделей производственных, логистических, финансовых и управленческих процессов для анализа эффективности, выявления узких мест и поиска оптимальных решений.
КОМАНДА И ПАРТНЕРЫ
- Синцова Ксения АнатольевнаРуководитель лаборатории. Кандидат математических наук, доцент ИИКС НИЯУ МИФИ.
Область исследований: математическое моделирование, формальная верификация сложных систем, теория доказательств. - Турянский ПавелИсследователь
- Кудасов НиколайИсследователь.
Университет Иннополис. - Соколов ПавелИсследователь.
Центральный университет. - Рословцев ВладимирИсследователь.
НИЯУ МИФИ. - Зайцев ВладиславИсследователь.
НИЯУ МИФИ.
Проекты лаборатории:
Построение формальной математической модели межсетевого экрана нового поколения (NGFW).
1
4
Гомотопическая теория групп
3
2
6
Лямбда - исчисление
5
Теория категорий
ИНСТРУМЕНТЫ и курсы
КОНТАКТЫ
+7 911 211 52 43
kseniasintlead@gmail.com
kseniasintlead@gmail.com
Москва, Каширское шоссе 31.
