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

Про первоначальный этап данного проекта можно прочитать в статье по ссылке:

https://system-informatics.ru/files/article/matrix_multiplication_verifi...

Данный проект открыт для присоединения новых участников. Для присоединения к данному проекту нужно пройти Летний Системный Буткемп Лаборатории YADRO НГУ. Более подробно о Летнем Системном Буткемпе Лаборатории YADRO НГУ написано по следующей ссылке:

https://www.nsu.ru/n/information-technologies-department/media/news/4423...

Отдельно отметим, что студентам ММФ НГУ, безусловно, тоже можно участвовать, участие студентов ММФ НГУ приветствуется. Летний Системный Буткемп Лаборатории YADRO НГУ пройдет с 17 августа по 29 августа.
Для регистрации на Летний Системный Буткемп Лаборатории YADRO НГУ нужно, войдя в предоставленный НГУ google-аккаунт, заполнить форму по ссылке:

https://forms.gle/wYRTk7D4i6p1mdpq8

В мотивационной части формы нужно написать о желании заниматься формальной верификации оптимизированных реализаций умножения матриц.
Прошедшие Летний Системный Буткемп Лаборатории YADRO НГУ могут получить специальные стипендии от компании YADRO.
Сегодня идут последние сутки для регистрации на Летний Системный Буткемп Лаборатории YADRO НГУ, поэтому нужно зарегистрироваться сегодня 10 июня.
По итогам проекта планируются научные публикации, а также возможна подготовка и защита выпускных квалификационных работ бакалавров и магистров.