This is a formal matrix library in Coq, and integrated with multiple different implementations.
Our goal is to provide a unified framework for different implementations of formalized matrix libraries, so as to decouple the differences between underlying technologies and upper-level applications.
CoqMatrix project CoqMatrix github
opam install coq-matrix
FinMatrix is a formal matrix library in Coq, which we started from finite sets (over natural numbers), vecotr based on finite sets, and matrices based on vectors. This implementation differs from the CoqMatrix project, which have various models. We have formalized many algebraic and geometric vector or matrix theories, especially including two inversion matrix algorithms: minvGE (inversion based on Gauss Elimination), minvAM (inversion based on Adjoint Matrix).
The details can be found in : FinMatrix Project FinMatrix github
OrienRepr is a formal verification project in Coq, for "Orientation Representation (OR)" problem, which is focused on derivation of popular models or algorithms for OR, including Euler Angles, Rotation Matrices, Axis-Angles, and Unit Quaternion.
The details can be found in : OrienRepr Project OrienRepr github
The VQCS is a formal verification project in Coq, which stands for "Verified Quantity Calculus System". We have modeled physical quantities, units, and dimensions, supporting calculations with units, and provide support for the International System of Units (SI), thereby enabling the verification of issues related to units.
The details can be found in : VQCS Project VQCS github
GenProg is an advanced code generation tool developed to convert verified Coq models into efficient and reliable C code.
Built on the language of DPIA (Data Parallel Idealised Algol), GenProg facilitates the seamless translation of high-level functional models into practical, executable programs.
This tool is particularly valuable for applications requiring stringent correctness guarantees, such as flight control systems, ensuring the consistency and reliability of the generated code.
GenProg is an essential resource for developers and researchers working on high-assurance systems, providing a robust solution for code generation from formally verified models.
The details can be found in : GenProg Project GenProg github
Verified Flight Control System (VFCS) is an academic project for study the FCS software by theorem prover Coq. We adopt the idea of construct-correct to analysis, modeling and design the FCS. Coq proof assistant is a higher-order logic theorem prover based on Calculus of Inductive Constructions. We mainly study the Multicopter at the first stage.
The details can be found in : VFCS project VFCS github