help@sochisirius.ru

Дискретные методы синтеза и верификации для киберфизических систем

Сроки проведения образовательного модуля изменены.

О новых сроках будет сообщено дополнительно

Программа пройдет в дистанционном формате
Прием заявок для участия в конкурсном отборе открыт до 4 мая 
2021 года
По вопросам участия в программе просим обращаться по адресу students@sochisirius.ru

Участники и порядок отбора

На обучение по программе дополнительной образовательной программы приглашаются студенты старших курсов бакалавриата, магистратуры и аспиранты, знакомые с основами дискретной математики и обладающие навыками программирования на языке Python.

Тематика программы соответствует следующим укрупненным группам специальностей:
01.00.00 Математика и механика
02.00.00 Компьютерные и информационные науки
09.00.00 Информатика и вычислительная техника
27.00.00 Управление в технических системах

Форма организации отбора обучающихся:
Индивидуальный отбор.
Оценивание резюме и мотивационного письма.

Также мы просим участников отбора предоставить нам следующие документы:

Справка с места обучения или диплом, если вы уже окончили обучение;

Сертификаты пройденных курсов/программ (при наличии);

Научные публикации, относящиеся к тематике образовательного модуля (при наличии);

Диплом о предыдущем уровне образования (при наличии).

Общее число обучающихся по программе – до 30 чел.

О программе

Программа знакомит слушателей с основами устройства современных промышленных киберфизических систем, а также с подходами к обеспечению их надежности, основанными на методах дискретной оптимизации. Даются вводные знания в области теории сложности, современных методов решения задачи выполнимости булевой формулы (SAT), применения SAT-технологий для решения прикладных задач, формальной верификации. Лекционный материал дополнен практическими занятиями по формальной верификации киберфизических систем и применению SAT-технологий в задачах синтеза и верификации.

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

Цель:
Познакомить обучающихся с устройством современных киберфизических систем, современными методами дискретной оптимизации на основе подходов к решению задачи выполнимости булевой формулы, методам формальной верификации; вовлечь обучающихся в научную деятельность.

Задачи:
- познакомить обучающихся с основными алгоритмами и методами дискретной оптимизации и формальной верификации, парадигмами и моделями киберфизических систем;
- сформировать у обучающихся знания, умения и навыки применения методов дискретной оптимизации к решения сложных комбинаторных задач.

В результате изучения курса, обучающиеся будут знать:
- основные принципы организации современных распределенных киберфизических систем;
- основы теории сложности;
- алгоритмические основы методов решения задачи булевой выполнимости (SAT), максимальной выполнимости (MaxSAT), выполнимости формул в теориях (SMT);
- основные алгоритмы и методы формальной верификации, в том числе явной и символьной;
- практические навыки по формальной верификации с помощью nuXmv;
- практические навыки по применению SAT-решателей.

Руководитель программы

Чивилихин
Даниил Сергеевич

к.т.н., доцент Университета ИТМО, руководитель лаборатории “Дискретная оптимизация и формальные методы”.

Преподаватели

Вяткин
Валерий Владимирович

д.т.н., профессор Университета ИТМО, профессор Университета Аалто (Финляндия), профессор Технического Университета Лулео (Швеция), IEEE senior member.

Чивилихин
Даниил Сергеевич

к.т.н., доцент Университета ИТМО, руководитель лаборатории “Дискретная оптимизация и формальные методы”.

Ульянцев
Владимир Игоревич

к.т.н., доцент Университета ИТМО, руководитель международного научного центра “Компьютерные технологии”.

Чухарев
Константин Игоревич

программист Университета ИТМО.

Овсянникова
Полина Александровна

аспирант Университета ИТМО и Университета Аалто.

Условия участия

Программа пройдет в дистанционном формате.

Партнеры

Образовательные организации высшего образования:

Национальный исследовательский университет ИТМО, https://www.itmo.ru/

Образовательный фонд "Талант и успех", https://sochisirius.ru/

Подать заявку
© 2015–2021 Фонд «Талант и успех»
Нашли ошибку на сайте? Нажмите Ctrl(Cmd) + Enter. Спасибо!