AdaCore + Automotive

AdaCore’s technology enables developers working on critical automotive applications to improve and streamline their development, verification, and certification processes.

Competition in the automotive industry is intense, and successful companies must constantly innovate by introducing new advances in software. The cars we drive today have large, growing amounts of sophisticated software aboard, controlling everything from the powertrain, to the suspension, braking, and entertainment systems. By some accounts, the number of lines of code in a luxury automobile is greater than the number of lines of code in a modern commercial jetliner.

Accompanying an increase in the complexity of automotive software, in particular when it comes to automated systems such as ADAS or autonomous driving which can have a strong impact on safety, the industry is raising the bar in terms of software quality and assurance. The evolution of the ISO-26262 safety standard is a good indication of this trend. This increase in system reliability requirements comes with an increased cost however. AdaCore solutions are positioned to mitigate this increase and offer alternatives and compliments traditional C development and heavy-testing based processes.

Reduce recalls with cost-effective software assurance.

AdaCore believes that the most cost-effective way to address safety and security needs is to address these requirements as early as possible in the development process, and has designed its toolset to allow software verification to take place as close as possible to the developper’s desk.

AdaCore’s tools and services for automotive are based around two components that can be used either independently or collaboratively:

Spark Pro Square

SPARK is a programming language and toolsuite that allows specification, development and verification of the software in the same language. The introduction of defects is minimized thanks to the  the intrinsic properties of the language. Dedicated static analysis tools can then formally demonstrate the absence of certain categories of defects and compliance of the code to pre-defined specifications.

ISO 26262

ISO 26262 is an international safety standard that encourages the use of system and software development processes to improve the safety of automotive systems. It provides requirements at various levels, through the whole development cycle, articulated around 4 risk levels (or ASIL) depending on the contribution of a given component to the overall safety. A large emphasis is dedicated to the verification processes, which includes activities such as reviews, testing and static analysis at the software level.

Three of AdaCore's signature software development/verification tools for Ada, SPARK and C have been qualified under the ISO 26262 and IEC 61508 functional safety standards.

AdaCore's GNAT Pro compiler and CCG have received TCL3 qualification under ISO 26262, and T3 qualification under IEC 61508. The SPARK Pro verification tool received TCL3 and T2 qualification. All three products have been certified by TÜV SÜD, an independent, globally recognized organization which confirms that products meet national and international standards. The TÜV SÜD certification mark is widely acknowledged and respected as a trusted symbol of quality, safety, and sustainability.

AdaCore has over two decades of certification experience in safety-critical domains such as avionics, space, and rail. By completing the qualification process for automotive and industrial standards, the company has shown that its high integrity technologies can meet the demanding assurance requirements of the software-intensive automotive industry.

Customer Projects: Automotive

View all customer projects »

AdaCore offers a variety of tools that have been tested and proven across the most demanding industries, making our products the ideal solution for developers that need to build safe, secure and reliable automotive applications.


SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.

GNAT Pro Assurance

GNAT Pro Assurance includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues. It supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems.

GNAT Static Analysis Suite

GNAT SAS helps developers gain a deep understanding of their code and build more reliable and secure software systems. GNAT SAS features an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs and vulnerabilities before program execution, serving as an automated peer reviewer, helping to find errors easily at any stage of the development life-cycle. It helps you improve the quality of your code and makes it easier for you to perform safety and/or security analysis.


GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)