AdaCore + Avionics

AdaCore has a long and successful history serving customers in the Avionics industry. Our products help developers build and verify software systems that meet the highest levels of safety certification.

On average, more than 8 million people worldwide fly in commercial airplanes every day. That’s over 3 billion passengers a year. Yet air travel continues to be our safest mode of transportation. This is in great part due to the fact that the Avionics industry has set the most stringent requirements for the development of safe and reliable software. 

Meeting DO-178 requirements is often a challenging and expensive process. AdaCore has years of experience working with avionics customers and has a deep understanding of the complexities of the certification process and tools needed to ease the workflow and manage costs.

Our Roots in Certification - Levels A and B in DO-178B / DO-178C

The company has extensive knowledge of and experience with avionics software certification standards, with AdaCore personnel playing an active role in standards-related working groups and committees. AdaCore President and co-founder Dr. Cyrille Comar is a recognized expert in software certification and participated in the development effort for DO-178C and its associated supplements.

Learn more about DO-178 »

Qualified Tools, Runtime Libraries and Certification Materials

Several of our tools have been qualified, thus reducing the effort to meet verification objectives including coding standard compliance, code accuracy (prevention of errors such as buffer overrun, integer overflow, and references to uninitialized variables), and structural coverage analysis up to MC/DC. Specialized high-assurance run-time libraries, including one that implements the Ravenscar tasking profile, are simple enough to be included in certified systems but expressive enough to support the needed functionality for hard real-time avionics software. Qualification and certification material for these tools and libraries is available and is adaptable to new project contexts.

Sustained Branches

Maintaining certified software brings unique challenges, since the customer needs to "freeze" on a specific version of the technology for stability, but still might require updated releases if a problem is encountered as the software evolves. AdaCore's "sustained branch" service, a standard part of the GNAT Pro assurance product, supports this requirement consistent with the guidance in DO-178B / DO-178C.

Customer Projects: Avionics

View all customer projects »
Ada Core Technologies For D0178

AdaCore Technologies for DO-178C / ED-12C

The guidance in the DO-178C / ED-12C standard and its associated technology-specific supplements helps achieve confidence that airborne software meets its requirements. Certifying that a system complies with this guidance is a challenging task, especially for the verification activities, but appropriate usage of qualified tools and specialized run- time libraries can significantly simplify the effort. This document explains how a number of technologies offered by AdaCore – tools, libraries, and supplemental services – can help.

Read our booklet »

AdaCore offers a variety of tools and services that ease the workflow and help reduce the costs for DO-178B/C certification. The cornerstone is GNAT Pro Assurance, a complete Ada development environment specially oriented towards critical systems.

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.


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 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)