AdaCore vehemently verifies (software) verification

Software development and verification tools company AdaCore has pushed out four product releases in line with the Embedded World Conference in Nuremberg this month.

Vehemently verifying verification

The firm has detailed GNAT Pro 17.1, a development environment for Ada and C on native and cross platforms; CodePeer 17.1, a deep static analysis tool for Ada that can identify bugs and vulnerabilities both during development and retrospectively on existing code bases; QGen 17.1, a model-based development and verification toolset for Simulink and Stateflow models, which generates code in MISRA-C or SPARK; and SPARK Pro 17.1, a verification environment that brings mathematics-based assurance to high-integrity software.

Why verification matters

“Developing and verifying critical systems is a challenging task, especially when certification against software standards such as DO-178C or EN 50128 is required,” said Cyrille Comar, AdaCore president.

“The latest version of our products will help organisations meet this challenge, through enhancements such as QGen’s model-level debugger and CodePeer’s detection of dangerous CWE weaknesses. Customers have long relied on AdaCore’s tools and services when producing safety-critical or high-security software, and our V17.1 product line marks a continuation of our commitment.”

GNAT Pro includes a build toolset for Ada and C, Integrated Development Environments (the GNAT Programming Studio (GPS) and the Eclipse-based GNATbench), a suite of tools (a visual debugger, a coding standard checker, etc.), and a set of libraries and bindings

CodePeer is an Ada source code analyser that detects run-time and logic errors, including a number of weaknesses among the Common Weakness Enumeration (CWE) Top 25 Most Dangerous Software Errors.

QGen is a qualifiable and tunable code generator and model verification toolsuite for a safe subset of Simulink and Stateflow models, particularly oriented towards real-time control software in safety-critical systems.

SPARK Pro is an integrated static analysis toolsuite for verifying high-integrity software through formal methods.

All V17.1 products are available now. F