关键词: 形式化验证, 形式化工程数学, 逆矩阵形式化, Coq, 软件安全

Abstract: Matrix is a data structure widely used in computer science,and its correctness of operation is of great significance.In matrix formalization,there is no reasonable and practical formalization work.The reason lies in the difficulty in formalizing the two common inverse methods in engineering.The first method is based on the adjoint matrix solution method.The difficulty lies in that the submatrices of n*n matrix cannot be formally expressed,which makes it very difficult to construct the matrix composed of cosubformulas.Therefore,it is difficult to achieve the formalization of adjoint matrix inverse solution.The second method is called Gauss-Jordan elementary transformation method,the difficulty lies in the construction of elementary matrix and its operation function.If Coq is used to design the operation function of inductive structure,that is,the idea of filling two-dimensional table with rows first is adopted,the description information of two-dimensional table from column dimension will be discarded,so that the operation function branches too much and complex inductive structure needs to be designed,which leads to the failure of subsequent formal verification.In this paper,a record-based matrix function construction method is proposed,which describes the matrix in both column and column dimensions,making it possible to construct and prove the elementary matrix.On this basis,the formalization of matrix inversion in Coq system based on gaussian-Jordan elimination method is realized.And we implement the first software matrix inversion function library under formal verification in a way with lower cost and time complexity.

Key words: Formal verification, Formal engineering mathematics, Inverse matrix formalization, Coq, Software security