AdaCore

Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a modern programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology.

Recently launched, SPARK Pro is an Integrated Development Environment for High-Assurance software, comprising Praxis’ SPARK language and toolset integrated into AdaCore’s GNAT Programming Studio (GPS). The SPARK Pro tools help prevent, detect, and eliminate defects early in a system’s life cycle, as the source code is developed. Frontline support is provided through GNAT Tracker, AdaCore’s web-based support system.

Designed by Praxis, SPARK is an Ada subset extended with a contract language that allows a program’s specification to be precisely expressed and verified. The SPARK language is especially suitable for applications where correct operation is vital for reasons of safety, security, or both. The SPARK toolset performs static (before run time) verification that is unrivalled in terms of its soundness, low false- alarm rate, depth, and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case to meet the requirements of industry regulators and certification schemes.

GNAT Pro and SPARK Pro has been used to build software applications to the highest safety and security levels in industries ranging commercial aircraft avionics, military systems, air traffic management/ control, railway systems and medical devices, and in security- sensitive domains such as financial services. For more info, please visit www.adacore.com/home/products or contact sales@adacore.com.