Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

Serra Z. Dane, Jiawei Chen, Marc Pouzet +1

Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of…