Beyond the boundaries of C: writing ASIL-4 software with verification-centric language —SPARK Ada and Formal Proof

Developing high integrity software at the highest level of safety (ASIL-4) requires the introduction of expensive specification and verification techniques. C and C++ as programming languages aren’t designed to accompany these processes and requires a lot of tooling and work to achieve the right level of confidence. This webex will develop an alternative approach based on the Ada programming language and the SPARK formal proof enfornment, showing how using coding techniques built for verification can reduce high-integrity software development and increase overall reliability and time-to-market.

• Overview of the Ada and SPARK programming languages
• Understanding Formal Proofs and how they differ from traditional static analysis
• Mixing Ada and SPARK together with legacy C code
• ISO-26262 considerations and benefits
• Industrial references