Skip to content

Latest commit

 

History

History
32 lines (26 loc) · 1.13 KB

README.md

File metadata and controls

32 lines (26 loc) · 1.13 KB

INTRODUCTION

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.

Note that, project OrienRepr is part of project VFCS (Verified Flight Control System), but it is not published for now.

The entrance of the project is OrienRepr/OrienRepr.v. For more details of different ORs, please check:

  • RotationMatrix3D.v
  • EulerAngle.v
  • AxisAngle.v
  • Quaternion.v

Resources

Preparation

This project need FinMatrix library, which is a formal matrix library in Coq, and also developed by us.

  • There are two ways to install FinMatrix
    • For stable version, use opam. opam install coq-finmatrix
    • For newest version, use source code. download the source code from FinMatrix github, then make; make install

Compile

make
make clean
make html