Во вторник 5 мая 2026 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).
Время проведения: 17.30-19.00 НСК (13.30-15.00 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Докладчик: Матвей Сергеевич Агибалов (студент ММФ НГУ)
Тема: На пути к дедуктивной верификации реализаций умножения матриц с направленными на повышение эффективности использования кэш-памяти оптимизациями.
Задача повышения производительности умножения матриц является актуальной задачей современного программирования. При решении данной задачи в программном коде умножения матриц реализуют оптимизации, что затрудняет анализ полученных реализаций и может приводить к появлению в них ошибок. Гарантировать корректность программного кода относительно спецификаций, описывающих результат работы программы в зависимости от ее входных данных, может только дедуктивная верификация. Итого, задача дедуктивной верификации реализаций умножения матриц с направленными на повышение производительности оптимизациями является актуальной. В данном докладе будет представлен первоначальный этап исследования, нацеленный на дедуктивную верификацию реализаций классического умножения матриц с направленными на повышение эффективности использования кэш-памяти оптимизациями.