Reliability with Formally Proven SPARK Ada
Ada and its subset SPARK is a language initially inspired by Pascal, embedding capabilities to describe specification, implementation and verification all in one platform. This unique integration allows identification and correction of defects early in the development cycles, reducing effort during late phases of development and mitigating risks of errors found after deployment. It can be used from large server environments running dozens of cores on gigabytes of memory down to bare metal small 8 bits microcontrollers below one megabyte, across architectures as diverse as x86, ARM, PowerPC or RISC-V.
Generates Code that is Formally Verified to be Free of Vulnerabilities
The Ada programming language and its SPARK subset combined with its toolset is a platform that allows developers to formally guarantee properties of source code, such as the 100% absence of certain categories of vulnerabilities (buffer overflow, division by zero, references to uninitialized variables, memory corruption), and to prove custom functional assertions.
Increases Critical Code Performance
SPARK and Ada provide performance levels and footprints similar to other system-level languages such as C. However, SPARK allows the removal of proven checks from the final binary, reducing the need for defensive code and allowing for safer and more efficient code execution.
Reduces Development Costs
The demand for cost-effective tools and methodologies has greatly increased in the automotive and industrial domains over the past few years. Using Ada and SPARK reduces the cost of developing safety and security-critical software by automating many verifications that would otherwise need to be done through manual code reviews or testing. It also allows the detection of potential issues early in the development process, reducing the amount of errors needing to be fixed in later stages. For industries that have strong safety, reliability, and security standards, like aerospace and automotive, these benefits can translate to nearly 40 percent cost and time savings from enhanced software verification, according to a study by VDC Research.
Large Open-Source Community
The Ada community is passionate about building dependable, high-integrity software. There are a number of resources available to academics, free software developers, or people who just want to learn more about Ada and would like to dive in right away.
An interactive learning platform designed to teach the Ada and SPARK programming languages is available at learn.adacore.com