New York,  NY 
United States
  • Booth: 2951

Tools for building mission-critical drone software.

AdaCore provides tools and expertise for the development of mission-critical, safety-critical, and security-critical software. AdaCore's flagship products are the GNAT Pro and SPARK Pro development environments and the CodePeer automatic code reviewer and validator. The GNAT Pro development environment includes all tools (code coverage and profiling, code standard checker, documentation generator, source code metrics, etc.) necessary for building robust and reliable applications. It provides support for a number of commercial RTOSes and bare board configurations. Customers around the world, including major actors in the mil-aero industry, trust GNAT Pro and AdaCore.

Brands: GNAT Pro Development Environment


  • GNAT Pro Development Environment
    The GNAT Pro development environment is a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability. For more information, please visit

  • Technical Features:


       - Full Ada implementation (Ada 2012, Ada 2005, Ada 95, and Ada 83), including all Specialized Needs Annexes


       - GPS (GNAT Programming Studio), a powerful, extensible and tailorable Integrated Development Environment


       - Visual debugging support, including a remote interface for debugging an embedded target


       - Stack usage analysis tool (GNATstack)


       - Compiler switch to help traceability of source to object code, for GNAT Pro Safety-Critical product (-fpreserve-control-flow)


       - Coding standard verification tool (GNATcheck)


       - Additional tools, including a heap usage monitor, a unit testing framework, a pretty printer, a program browser, an HTML generator, and a program metrics generator


       - Libraries and binding supplementing the standard Ada API, including packages for services such as operating system interfaces, text manipulation and pattern matching, data structures and algorithms, and I/O operations


       - Detailed and understandable documentation, including the GNAT Pro User’s guide and GNAT Pro Reference Manual

  • CodePeer Static Analysis Tool
    The CodePeer static analysis tool is a source code analyzer that detects run-time and logic errors. For more information, please visit

  • - Uses static control-flow, data-flow, and possible-value-set propagation techniques to detect errors before program execution


    - Mathematically analyzes every line of code without executing the program, considering all combinations of program input across all paths within the program


    - Analyzes programs for a wide range of flaws including:

           pointer misuse

           buffer overflow

           numeric overflow

           division by zero

           dead code

           use of uninitialized data

           concurrency faults (race conditions)


    - Identifies not where where a failure could occur, but also where the bad values originate

           withing the current subprogram

           from some non-local subprogram that reached the point of failure through a series of calls


    - Detects code that, although syntactically and semantically correct, is performing a suspect computation such as

           assigning to a variable that is never subsequently referenced

           testing a condition that always evaluates to the same true or false value


    - Automatically generates both human-readable and machine-readable component specifications

           preconditions and postconditions

           inputs and outputs

           heap allocations

  • QGen
    QGen is a qualifiable and tunable code generation and model verification tool for a safe subset of Simulink® and Stateflow® models. For more information please see

  • QGen answers once core question: How can I decrease the verification costs when applying model-based design and automatic code generation with the Simulink® and Stateflow® environments?  This is achieved by


         1.  Selecting a safe subset of Simulink® blocks

         2.  Ensuring high-performace and tunable code generation

         3.  Relying on static analysis for upfront detection of potential errors, and

         4.  Providing top-class DO-178B/C, EN 50128nand ISO 26262 qualification material for both the code generator and the model verification tools.


    QGen also decreases tool inegration costs by integrating smoothly with AdaCore's qualifiable compilation, simulation and structural coverage analysis products.

  • SPARK Pro
    SPARK Pro is an integrated static analysis toolsuite for developing and verifying high-integrity software. For more information, please visit

  • - Soundness

         The toolset can perform a wide range of static verification functions.  Analysis with the SPARK Pro toolset is sound (no "false negatives"): if no errors of a certain type are reported then none are present in the program.  Soundness is essential for static analysis tools to be used in verifying critical systems.


    - Ultra-Low False Alarm Rate

         Other languages and toolsets often exhibit a high false alarm rate that makes them of little practical use.  With SPARK the nature of the langage minimuzes the number of false alarms that are reported, allowing users to focus more easily on genuine defects.


    - Modularity

         SPARK is a modular langage and the SPARK tools can be used incrementally during system development.  There is no need to wait until a program is complete before obtaining deep and useful analysis results.


    - Hybrid Verification

         Hybrid Verifcation is an innovative approach to demonstrating the functional correctness of a program using a combination of automated proof and unit testing.  Only where verification cannot be completed automatically is it necessary to write unt tests -- using the same contracts to check the correct run-time behavior of the relevant subprograms.


    - Ease of Transition to SPARK 2014

         For customers with an established SPARK code base, a tool is provided to assist with the translation process.  Once translated into SPARK 2014, the code can be extended to take advantage of new features in the new expanded language and advanced toolset.


    - Integrated Target Parameterization

         For embedded systems where cross-compilation is used, SPARK Pro automatically integrates with GNAT Pro to read the configuration of the target.  This guarantees that the verification performed by the tools remains sound for the run-time target environment.