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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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