Future work

 -  Express functional properties of the controller interacting with its environment at the level of the code, and prove them.
 -  Develop suitable abstract domains of ellipsoids for static analysis
 -  Study the effect of various model transformations on the validity of the proof (e.g. from an abstraction standpoint):
    • Discretization
    • Floating-point arithmetic
    • Machine-level constructs (pointers)
 -  Automatize the process by which annotated C code gets proven with PVS.