Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems.

Over the years, customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial and military avionics, automotive, railway, space, defense systems, air traffic management/control, medical devices, and financial services. AdaCore has an extensive and growing worldwide customer base.

AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris.

Code Development

Build better software with our full-featured, multi-language (Ada, SPARK, C, C++) development environment that comes with unmatched product support and expert Ada consulting.

The GNAT Pro product line offers a comprehensive toolset for Ada, C and C++. Different versions of the product — GNAT Pro Assurance and Enterprise — support a wide range of project sizes and needs.

The integration of the LDRA tool suite with GNAT Pro helps embedded developers overcome the challenges of testing real-time Ada software in circumstances where applications are required to be reliable, rugged and as error free as possible. The LDRA tool suite also provides facilities to assist users to meet recognized Ada standards and subsets such as the Ravenscar Profile and the SPARK safe-subset for Safety-Critical and High-Integrity systems.

Formal Verification

Specify and automatically verify software architectural properties, and guarantee a wide range of software integrity properties including freedom from run-time errors, enforcement of security policies, and functional correctness.

SPARK Pro is a powerful language and toolset combination that brings mathematics-based confidence to software verification.

Model-Based Engineering

Streamline your development and verification processes for critical systems specified through Simulink® and Stateflow® models.

Reduce development and verification effort through QGen, a qualifiable and customizable code generator and model verifier/debugger for a safe subset of Simulink® and Stateflow® models. QGen generates source code in SPARK or MISRA C.

Qualification and Certification Material

AdaCore has a long history of serving the safety-critical software development community. Customers have used our products and services to implement, verify and maintain systems that meet the highest levels of domain-specific software standards such as: