
Application: Quanser 3-degree-of-freedom Helicopter

- We intend to use this pedagogical tool to showcase the fully verified process from annotated diagram to binary code running the engines.
- At this point we successfully generate annotated C code expressing the controller stability.