О ЛАБОРАТОРИИ
НАПРАВЛЕНИЯ ИССЛЕДОВАНИЙ
ОТКРЫТЫЕ МАТЕРИАЛЫ И КУРСЫ
УСЛУГИ БИЗНЕСУ
КОМАНДА
КОНТАКТЫ
  • Лаборатория формальной математики и доказательств
Formal Mathematics and Proofs LAB
Национальный исследовательский ядерный университет «МИФИ»
Институт интеллектуальных кибернетических систем
Математическое Моделирование и верификация киберсистем
LOGO
MENU
О ЛАБОРАТОРИИ
Лаборатория математического моделирования, логики, теории категорий, формальных методов доказательства.
Мы занимаемся исследованием и математическим моделированием киберфизических систем. Решаем задачи верификации и доказательства корректности работы различных систем по заданным спецификациям требуемой проверки.
Формальная верификация
Математическое доказательство того, что рассматриваемая система (киберсистема) полностью соответствует заданным формальным требованиям/спецификации.
01
Математическое моделирование киберсистем
Создание и анализ математической модели объекта или процесса для изучения его поведения, прогнозирования наблюдаемых результатов и последующее принятий решений.
02
Гомотопическая теория типов
Математическая теория, рассматривающая типы, как геометрические объекты и использующая методы алгебраической топологии для формального описания и доказательства математических утверждений.
03
Теория доказательств. Логика
Раздел логики, исследующий методы построения математических доказательств, а также их доказуемость.
04
Функциональное программирование
Стиль создания кода, где программы строятся исключительно на основе математических функций и неизменяемых данных.
05

Направления исследований
Методы формальной верификации в системе Rodin. Введение
1
4
Гомотопическая теория групп
3
RZK proof assistant
2
Верификация на Rocq (coq)
6
Лямда исчисление
5
Теория категорий
Открытые материалы и курсы

УСЛУГИ БИЗНЕСУ

  • Компьютерное моделирование и прогнозирование
    Создание имитационных моделей для оценки рисков, прогнозирования результатов управленческих решений и выбора наиболее эффективных стратегий развития бизнеса.
  • Верификация и проверка надежности киберсистем и алгоритмов
    Независимая экспертиза корректности работы киберфизических систем, программных алгоритмов и инженерных решений с оценкой корректности, устойчивости и соответствия заданным требованиям.
  • Оптимизация процессов на основе методов искусственного интеллекта и математического анализа
    Разработка алгоритмов оптимизации затрат, ресурсов, производственных планов и логистических цепочек с использованием современных математических методов.
  • Математическое моделирование бизнес-процессов и систем
    Разработка цифровых моделей производственных, логистических, финансовых и управленческих процессов для анализа эффективности, выявления узких мест и поиска оптимальных решений.
Проекты лаборатории:
Построение формальной математической модели межсетевого экрана нового поколения (NGFW).

КОМАНДА

  • Синцова Ксения Анатольевна
    Руководитель лаборатории. Кандидат математических наук, доцент ИИКС НИЯУ МИФИ.
    Область исследований: математическое моделирование, формальная верификация сложных систем, теория доказательств.
  • Турянский Павел
    Исследователь
  • Кудасов Николай
    Исследователь.
    Университет Иннополис.
  • Соколов Павел
    Исследователь.
    Центральный университет.
  • Рословцев Владимир
    Исследователь.
    НИЯУ МИФИ.

  • Зайцев Владислав
    Исследователь.
    НИЯУ МИФИ.

КОНТАКТЫ

+7 911 211 52 43
kseniasintlead@gmail.com
Москва, Каширское шоссе 31.
Attention!
This template requires Arial font. Set it up before using this template.
Heading font: Arial
Body text font: Arial

How to set up font:
1. Go to Site Settings → Fonts and Colors
2. Select Arial font and save changes

See the original page design here: https://photolab-template.tilda.ws
Made on
Tilda