Towards deductive verification of matrix multiplication implementations with cache-efficient optimizations

Improving the performance of matrix multiplication is a pressing issue in modern programming. When solving this problem, optimizations are implemented in the matrix multiplication code, which complicates the analysis of the resulting implementations and can lead to errors. Only deductive verification can guarantee the correctness of the code relative to the specifications describing the program's output based on its input data. Therefore, the problem of deductive verification of matrix multiplication implementations with optimizations aimed at improving performance is relevant. This article presents the initial stage of research aimed at deductively verifying implementations of classical matrix multiplication with optimizations aimed at improving cache memory efficiency.