AdaCore’s offerings are geared towards developers of embedded and native applications that demand high levels of assurance. Such software is written in a variety of programming languages, which AdaCore supports through compilers, multi-language build tools, IDEs, debuggers, and static and dynamic analysis tools.
The Ada language has a long and successful history in high-assurance systems on both native and embedded platforms, combining reliability, maintainability and performance. AdaCore has been at the forefront of advanced Ada technology since the company’s inception, and our products support all versions of the language standard: Ada 83, Ada 95, Ada 2005, and Ada 2012.
SPARK is an Ada 2012 subset that supports formal proofs of program properties ranging from absence of run-time errors to functional correctness (compliance of the code with formally specified requirements). As such the language is appropriate for applications at the highest levels of safety and/or security. SPARK can be integrated with code in other languages, such as Ada, C, or C++, using hybrid verification that combines formal methods with traditional testing-based approaches.
C and C++
C remains the most common high-order language for embedded systems development, and in large applications C++ can bring the benefits of more powerful and expressive features while retaining C’s performance advantages. AdaCore’s gcc-based multi-language technology implements both C and C++, allowing programmers to develop software in either or both of these languages and, if applicable, integrate their code with Ada. AdaCore toolsets support C89 through C11 and C++89 through C++14.