Reduce Cost While Improving Safety and Security with Formal Methods Through Ada SPARK

There are three conflicting needs for teams that are building software systems that have to adhere to functional safety and security standards such as ISO 26262, IEC 61508, ISO 62443, R155 and others. Firstly, they have to adhere to very strict security standards, secondly, they have to deliver on-time and on-budget and lastly, they have to frequently deliver updates to deliver more functionality as well as fix any reported security issues.

In this presentation, we will walk through a small sample application in Ada SPARK and demonstrate how it delivers improved safety and security at lower cost in three steps:

• Firstly, memory safety and type safety removes a significant amount of runtime problems.
• In the second step, we will tighten the program to be able to prove the absence of runtime errors completely.
• In the third step, we will prove the correctness of the program.

The presentation will also touch on how companies like NVIDIA and Rolls Royce depend on Ada SPARK, enabling them to deliver safe and secure software at scale.

AdaCore provides tools for high-integrity development in Ada/SPARK, C/C++, and Rust. We equip developers to build reliable, safe, and secure software. With over 30 years of experience, we provide open-source toolchains for Ada/SPARK, C/C++, and Rust, designed specifically for safety-critical and mission-critical systems.

Our technology supports the world’s most demanding industries, including aerospace, defense, rail, automotive, energy, telecoms, finance, and medical. Built to meet rigorous certification standards, our tools let you focus on your code - with confidence.