Eric: Created page with "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” p..."

2014-02-14T20:19:30Z

Created page with "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” p..."

New page

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.

WG211/M13Franchetti - Revision history

Eric: Created page with "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” p..."