Formal Verification of Executable Matrix Inversion via Adjoint Matrix and Gaussian Elimination

Type Conference proceedings, EI

Date:Sep, 2024 Author: Zhengpu Shi, Gang Chen

Conference: PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming. Milan, Italy

DOI: 10.1145/3678232.3678242 Paper URL: online paper

Abstract: Matrix inversion algorithms are ubiquitous in engineering, computer science, and other disciplines. While formal verification exists for individual inversion methods, a comprehensive verification alongside directly executable algorithms within a theorem prover is lacking for two key methods: inversion via the adjoint matrix (InvAM) and inversion via Gaussian elimination (InvGE). This paper addresses this gap by offering constructive implementations and rigorous formal verifications of both InvAM and InvGE within the Coq proof assistant, thus enabling reliable and ready-to-use computation of matrix inverses directly in the Coq environment. To facilitate the verification process, we introduce FinMatrix, a formal model for matrices. This model defines a vector as a function from a finite set to a type of elements and encapsulates a matrix as a vector of vectors. We formalize a comprehensive set of operations and mathematical properties pertinent to vectors and matrices. Leveraging this foundation, we formalize determinant theory and the Gaussian elimination algorithm, essential components of the matrix inversion process. We then proceed to formalize the aforementioned matrix inversion algorithms, InvAM and InvGE. To demonstrate the practicality of our formal verification, we addressed a system of linear equations within Coq using three distinct methods: Cramer’s rule, and inversion via InvAM or InvGE. We also illustrated the process for determining the inverse of a symbolic matrix with partial automation. Furthermore, we extracted OCaml code from Coq and performed preliminary performance tests. Our formalized algorithms set a benchmark for verifying additional matrix inversion methods and lay the groundwork for formalizing more advanced matrix theories.

Cite format: Zhengpu Shi and Gang Chen. 2024. Formal Verification of Executable Matrix Inversion via Adjoint Matrix and Gaussian Elimination. In Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming (PPDP '24). Association for Computing Machinery, New York, NY, USA, Article 12, 1–13. https://doi.org/10.1145/3678232.3678242

Bib file: go to download page

Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and Quaternion

Type Conference proceedings, EI

Date:Sep, 2024 Author: Zhengpu Shi, Gang Chen

Conference: FACS 2024: 20th International Conference on Formal Aspects of Component Software. Milan, Italy

DOI: 10.1007/978-3-031-71261-6_5 Paper URL: online paper

Abstract: Rotation matrices, Euler angles, axis-angle, and unit quaternions are common models for representing object pose in space. Each offers distinct advantages and disadvantages regarding handling singularities, computational complexity, and storage requirements, motivating their interchangeability and conversion algorithms. However, these models and their associated algorithms involve complex matrix operations, trigonometric computations, and geometric reasoning, making manual derivation and verification error-prone. To guarantee algorithm correctness, we present a formal verification of these models and their conversion algorithms within the Coq Proof Assistant, focusing on pure rotational orientation representation. We establish a formal foundational mathematical library, including vector and matrix theories on abstract elements, additional real matrix properties, and quaternion theory. Building upon this foundation, we formalize all four rotation models and their conversion algorithms, emphasizing invariants of special orthogonal groups, Rodrigues’ rotation formula, and the quaternion rotation formula. Our formally verified library offers excellent readability, usability, and simplicity, laying a foundation for developers to understand and verify advanced kinematics algorithms.

Cite format: Zhengpu Shi, Gang Chen. (2024). Coq Formalization of Orientation Representation: Matrix, Euler Angles, Axis-Angle and Quaternion. In: Marmsoler, D., Sun, M. (eds) Formal Aspects of Component Software. FACS 2024. Lecture Notes in Computer Science, vol 15189. Springer, Cham. https://doi.org/10.1007/978-3-031-71261-6_5

Bib file: .BIB

CoqMatrix: Formal matrix library with multiple models in Coq

Type Journal Article, SCI (CAS Zone 2), CCF-B Journal

Date:Oct, 2023 Author: Zhengpu Shi, Guojun Xie, Gang Chen

Journal: Journal of Systems Architecture

DOI: doi.org/10.1016/j.sysarc.2023.102986 Paper URL: online paper

Keywords: Coq theorem prover, Formal matrix theory, Unified matrix interface, Matrix models comparison, Isomorphic mapping, Formal vector theory, Unified vector interface

Abstract: Matrices are common tools in mathematics and computer science, and matrix formalization in proof assistants can provide strong support for verifying system behaviors related to matrix operations. The Coq community has proposed at least five formal matrix models, although the Coq standard library does not implement them. Developers who require a formal matrix library could have difficulty choosing what model to use. More importantly, once a choice is made, switching to another model later can be expensive. Although these matrix models have formalized matrix theory to a certain scale, demonstrating the ability to support the development of matrix theory, they have not identified the absolute advantages over other models, making it difficult for developers to choose. Moreover, the models have different data structures with completely different signatures of function and theorem, forcing developers to virtually completely rewrite matrix-related scripts when switching to a new matrix model. To address these problems, herein we undertake the following. First, we propose a unified matrix interface and integrate existing formal matrix models in the Coq community based on this interface. Secondly, we construct bijective functions between the different models to form isomorphisms, thus establishing connections between these models. We also provide technical comparison conclusions to help developers make choices. Hence, matrix formalization developers have a reference guide in the early stage and can switch to other models at a low cost at a later stage or use multiple models simultaneously with conversion assistance.

Cite format: Zhengpu Shi, Guojun Xie, and Gang Chen. CoqMatrix: Formal matrix library with multiple models in Coq[J]. Journal of Systems Architecture, 2023, 143: 102986. https://doi.org/10.1016/j.sysarc.2023.102986

Bib file: .BIB

Integration of Multiple Formal Matrix Models in Coq

Type Conference proceedings, EI, CCF-C Conference

Date:Dec, 2022 Author: Zhengpu Shi & Gang Chen

Conference: SETTA 2022

DOI: 10.1007/978-3-031-21213-0_11 Paper URL: online paper

Abstract: Matrices are common tools in mathematics and computer science, and matrix formalization in proof assistants can provide strong support for verifying system behaviors related to matrix operations. The Coq community has proposed at least five formal matrix models, although the Coq standard library does not implement them. Developers who require a formal matrix library could have difficulty choosing what model to use. More importantly, once a choice is made, switching to another model later can be expensive. Although these matrix models have formalized matrix theory to a certain scale, demonstrating the ability to support the development of matrix theory, they have not identified the absolute advantages over other models, making it difficult for developers to choose. Moreover, the models have different data structures with completely different signatures of function and theorem, forcing developers to virtually completely rewrite matrix-related scripts when switching to a new matrix model. To address these problems, herein we undertake the following. First, we propose a unified matrix interface and integrate existing formal matrix models in the Coq community based on this interface. Secondly, we construct bijective functions between the different models to form isomorphisms, thus establishing connections between these models. We also provide technical comparison conclusions to help developers make choices. Hence, matrix formalization developers have a reference guide in the early stage and can switch to other models at a low cost at a later stage or use multiple models simultaneously with conversion assistance.

Cite format: Zhengpu Shi, Gang Chen. (2022). Integration of Multiple Formal Matrix Models in Coq. In: Dong, W., Talpin, JP. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2022. Lecture Notes in Computer Science, vol 13649. Springer, Cham. https://doi.org/10.1007/978-3-031-21213-0_11

Bib file: .BIB

多旋翼飞控推进子系统的Coq形式化验证

Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter

Type Journal Article, EI, CCF-A Chinese Journal

Date:June, 2022 Author: 石正璞,崔敏,谢果君,陈钢

Journal: Journal of Software (软件学报)

DOI: 10.13328/j.cnki.jos.006575 Paper URL: online paper

Chinese keywords: 形式化验证;定理证明;多旋翼飞行器;飞行控制系统;推进系统;Coq;Ocaml

Chinese abstract: 飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.

Cite format: Zhengpu Shi, Min Cui, GuoJun Xie, Gang Chen. Coq Formalization of Propulsion Subsystem of Flight Control System for Multicopter. Journal of Software, 2022,33(6):2150-2171

Cite format(中文): 石正璞,崔敏,谢果君,陈钢.多旋翼飞控推进子系统的Coq形式化验证.软件学报,2022,33(6):2150-2171

Bib file: .BIB