Skip to content

Formal verification of orientation representation in Coq

License

Notifications You must be signed in to change notification settings

zhengpushi/OrienRepr

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

28 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

Formal verification of orientation representation in Coq

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published