--- Overview Traditional control theorists are concerned with high-level control algorithms and their high-level properties such as convergence, robustness and performance. Notably, they typically assume all calculations are done with real numbers, and do not pay as much attention to the concrete implementation of their control algorithms, or to issues such as precise programming language semantics, or to errors introduced by machine arithmetic. In the CAFEE project, we aim to bridge the gap between control theory and low-level implementations, by providing typical control theory guarantees on the implementation rather than on a high-level algorithm. Overall, the CAFEE research project aims to achieve comprehensive end-to-end verification of control systems, encompassing high-level hybrid models down to the verification of embedded C code, thereby establishing a comprehensive framework for end-to-end verification of control systems. --- Intellectual Merit The CAFEE project will consist of 5 different work-packages. In the first work-package, we will provide an integrated approach for simple linear discrete-time systems, including the design of and end-to-end process achieving verification at all stages, with discrete-time plant semantics. In the second work-package, we will extend the work to focus on hybrid systems consisting of a continuous-time plant dynamics and a discrete-time controller one. While typical control engineers work either with pure continuous-time or pure discrete-time models for verification purpose, the actual system combines both paradigms. We will define a proper semantics model for these hybrid systems, and develop new verification means to reason on these closed loop systems. In the third work-package, we will consider control algorithms that rely on optimization routines, such as model predictive control. Little verification work has been done in this context, and we plan to leverage some of our recent work and develop verification techniques that can be applied to such optimization routines. Our fourth work-package will be an integration task that will focus on numerical accuracy using machine arithmetic, and will integrate the first three work-packages in this context. Verification will then be performed at model level and all along the development cycle, relying on autocoding and target the final hardware platform, considering numerical accuracy of computation. Finally our fifth work-package will apply our techniques on three different applications: car collision avoidance, aircraft collision avoidance, and spacecraft docking. --- Broader Impacts The CAFEE project will build a formal framework enabling full end-to-end verification of control algorithms, with respect to their formal specification. This framework will be released open-source and available to use by academic, government and industrial partners alike. We already work closely with several government agencies (CNES, NASA) and industrial partners (Collins Aerospace, Toyota), and will continue to do so to help with our design. Our government and industrial relationships will ensure technological transfer to those partners. We will also integrate the use of our framework in classes. Another broader impact of the project will be to bring closer together the formal methods community and the traditional control theory community. By bringing together those communities closer, we hope to raise awareness among the control community of such software issues as programming-languages arithmetic and machine precision (both fixed-point and floating-point). Conversely, the formal methods community will learn about the concerns of the controls community, as well as concrete ways to mitigate potential errors, such as using precise robustness measures in the design of control systems. The papers stemming from the project will be published and presented at a combination of formal methods venues and control theory venues.