The AdaCore Edge

Development and Verification Technologies for Software that Matters

Producing software for a modern cybersystem is hard. The system must not only be reliable and efficient, it has to be secure from threats both known and unknown, and also adaptable in the face of changing requirements and an evolving technological landscape. It may also need to comply with an industry-specific safety standard such as DO-178B or DO-178C for airborne systems. These challenges require programming languages, tools and support that developers can trust and exploit throughout the software life cycle. It’s especially important to catch bugs early, when they are least expensive to correct. AdaCore has been providing solutions in these areas for nearly 25 years, for customers across a range of critical domains including aerospace, rail, defense systems, automotive, medical devices and finance.

Multi-Language Software Development Environments

At the hub of AdaCore’s offerings are the GNAT Pro integrated software development environments, available for Ada and also C and C++.
GNAT Pro Ada handles all versions of the language standard, from Ada 83 through Ada 2012, and includes a comprehensive toolsuite, graphical IDEs, and extensive companion libraries. The product is available in several editions:
  • Assurance, which is especially applicable for Ada projects requiring certification or which need to remain on a specific version of the technology;
  • Enterprise, which is appropriate for any Ada project; and
  • Developer, which is geared towards projects migrating to Ada 2012 from C or C++.
GNAT Pro is also available for C and C++, with full support for these languages.

Formal Methods-Based Verification

The SPARK Pro toolsuite brings mathematical assurance to software verification. Taking advantage of the latest breakthroughs in automated proof technology, SPARK Pro performs sound static analysis on the formally analyzable SPARK subset of Ada 2012. It can prove program properties ranging from correct data flows and absence of run-time errors to full functional correctness, and can be combined with traditional testing-based verification techniques. SPARK Pro is especially applicable to systems demanding high security and/or safety, and it can be introduced incrementally into existing projects.

Deep Static Analysis for Ada

CodePeer is an advanced static analysis tool for Ada and can be used either as a “bug finder” to detect latent vulnerabilities in existing code bases, or during development to catch logic errors early. CodePeer has been designated as CWE-Compatible by the MITRE Corporation's Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program, and the tool can detect several weaknesses that are among the “Top 25 Most Dangerous Software Errors” in the CWE. Errors caught by CodePeer include buffer overflow, integer overflow/wraparound, references to uninitialized variables, useless assignment statements, dead code, and data race conditions.

Learn How AdaCore’s Products Can Help You

AdaCore has prepared a series of publications that explain how the company’s products can support software projects with the most demanding requirements: For a printed copy of any of these publications, please contact us at
Loading... Loading...