- Об университете
- Поступление
Поступление
- Исследования
- Медиа
Программа пройдет в дистанционном формате
По вопросам участия в программе просим обращаться по адресу students@sochisirius.ru
Программа знакомит слушателей с основами устройства современных промышленных киберфизических систем, а также с подходами к обеспечению их надежности, основанными на методах дискретной оптимизации. Даются вводные знания в области теории сложности, современных методов решения задачи выполнимости булевой формулы (SAT), применения SAT-технологий для решения прикладных задач, формальной верификации. Лекционный материал дополнен практическими занятиями по формальной верификации киберфизических систем и применению SAT-технологий в задачах синтеза и верификации.
Настоящая программа направлена на формирование у обучающихся базового набора компетенций об устройстве современных киберфизических систем, о современных методах дискретной оптимизации на основе подходов к решению задачи выполнимости булевой формулы, а также о методах формальной верификации. Приводятся примеры практических задач, в которых применяются методы формальной верификации и синтеза.
Цель:
Познакомить обучающихся с устройством современных киберфизических систем, современными методами дискретной оптимизации на основе подходов к решению задачи выполнимости булевой формулы, методам формальной верификации; вовлечь обучающихся в научную деятельность.
Задачи:
- познакомить обучающихся с основными алгоритмами и методами дискретной оптимизации и формальной верификации, парадигмами и моделями киберфизических систем;
- сформировать у обучающихся знания, умения и навыки применения методов дискретной оптимизации к решения сложных комбинаторных задач.
В результате изучения курса, обучающиеся будут знать:
- основные принципы организации современных распределенных киберфизических систем;
- основы теории сложности;
- алгоритмические основы методов решения задачи булевой выполнимости (SAT), максимальной выполнимости (MaxSAT), выполнимости формул в теориях (SMT);
- основные алгоритмы и методы формальной верификации, в том числе явной и символьной;
- практические навыки по формальной верификации с помощью nuXmv;
- практические навыки по применению SAT-решателей.
К.т.н., доцент Университета ИТМО, руководитель лаборатории “Дискретная оптимизация и формальные методы”
На обучение по программе дополнительной образовательной программы приглашаются студенты старших курсов бакалавриата, магистратуры и аспиранты, знакомые с основами дискретной математики и обладающие навыками программирования на языке Python.
Тематика программы соответствует следующим укрупненным группам специальностей:
01.00.00 Математика и механика
02.00.00 Компьютерные и информационные науки
09.00.00 Информатика и вычислительная техника
27.00.00 Управление в технических системах
Форма организации отбора обучающихся:
Индивидуальный отбор.
Оценивание резюме и мотивационного письма.
Также мы просим участников отбора предоставить нам следующие документы:
Справка с места обучения или диплом, если вы уже окончили обучение;
Сертификаты пройденных курсов/программ (при наличии);
Научные публикации, относящиеся к тематике образовательного модуля (при наличии);
Диплом о предыдущем уровне образования (при наличии).
Общее число обучающихся по программе – до 30 чел.
Программа пройдет в дистанционном формате.
Университет «Сириус» – это пространство, где студенты, ведущие ученые и представители российских технологических компаний объединяются, чтобы разрабатывать новые технологии и внедрять их в привычную жизнь. У каждого студента нашей страны есть возможность стать частью команды, которая меняет мир вокруг.
Специально для этого в «Сириусе» были созданы краткосрочные интенсивные программы, участниками которых могут стать студенты из всех регионов страны. Все программы созданы в партнерстве с ведущими компаниями и посвящены актуальным вопросам и направлениям в науке.
