На пути к дедуктивной верификации реализаций умножения матриц с направленными на повышение эффективности использования кэш-памяти оптимизациями

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