УмножениеМатриц22сен26

Докладчики: Кондратьев Дмитрий Александрович (ИСИ СО РАН, НГУ), Ануреев Игорь Сергеевич (ИСИ СО РАН, НГУ), Долгов Кирилл Андреевич (НГУ), Агибалов Матвей Сергеевич (НГУ), Харьков Александр Андреевич (НГУ), Бояндин Лев Константинович (НГУ), Чинахов Денис Дмитриевич (НГУ), Вишнякова Алиса Алексеевна (НГУ), Валентинова Авелиция Дмитриевна (НГУ) Тема: Дедуктивная верификация реализации умножения матриц с оптимизациями в виде изменения порядка вложенности циклов и векторизации внутреннего цикла с помощью ассемблерных вставок Аннотация: Задача повышения производительности умножения матриц является актуальной задачей современного программирования. При решении этой задачи в программном коде умножения матриц реализуют оптимизации, что может приводить к появлению ошибок в полученных реализациях и затрудняет их анализ. Дедуктивная верификация может гарантировать корректность программного кода относительно спецификаций, описывающих результат работы программы в зависимости от входных данных. В докладе будут представлены результаты проекта по дедуктивной верификации в системе Frama-C/WP реализации умножения матриц с оптимизациями, изменяющими порядок вложенности циклов с векторизацией внутреннего цикла с помощью ассемблерных вставок. Этот проект выполнен на Летнем Системном Буткемпе Лаборатории YADRO НГУ.