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.