WG211/M13Franchetti

High Assurance Spiral: Co-Synthesizing Proof and Implementation From High-Level Specification In this talk we introduce “High Assurance SPIRAL” to solve the “last mile” problem for the synthesis of high assurance implementations of controllers for vehicular systems that are executed in todays and future embedded and high performance embedded system processors. High Assurance SPIRAL is a methodology to translate a high level specification of a high assurance controller into a highly resource-efficient, platform-adapted, verified control software implementation for a given platform in a language like C or C++. High Assurance SPIRAL proves that the implementation is equivalent to the specification written in the control engineer's domain language. Our approach supports problems involving floating-point calculations and provides highly optimized synthesized code. At the core of High Assurance SPIRAL is the Hybrid Control Operator Language (HCOL) that leverages advanced mathematical constructs expressing the controller specification to provide high quality translation capabilities.