AdaCore provides a number of powerful tools that assist in the static verification of software properties such as code metrics, style checks or potential run-time errors.
CodePeer assesses a program for potential bugs before it is executed, in effect serving as an automated peer review. Using control-flow, data-flow, and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labor-intensive debugging.
SPARK Pro provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Altran with the GNAT Programming Studio (GPS) development environment from AdaCore. SPARK Pro prevents, detects and eliminates defects early in the life-cycle as the source code is developed.
Traceability Analysis Package
Source-to-object Code Traceability
A customized source-to-object code traceability analysis tool, GNAT Pro’s Traceability Analysis Package comprises an Ada language feature analysis, including test cases and GNAT Pro switch recommendations, that can help developers demonstrate compliance of safety-critical software with the DO-178B avionics standard. Learn More »
ASIS for GNAT
Ada Semantic Analysis
ASIS, the Ada Semantic Interface Specification, is a library that gives applications access to the complete syntactic and semantic structure of an Ada compilation unit. This library is typically used by tools that need to perform some sort of static analysis on an Ada program. Learn More »