AdaCore's GNAT Pro, CodePeer, QGen and SPARK Pro
All products aid organizations with the challenges they face in the development and verification of critical systems, especially when certification against software standards, such as DO-178C or EN 50128, is required. GNAT Pro is a development environment for Ada and C, on native and cross platforms. CodePeer is a deep static analysis tool for Ada that can identify bugs and vulnerabilities both during development and retrospectively on existing code bases. SPARK Pro is a verification environment that brings mathematics-based assurance to high-integrity software, and QGen is a model-based development and verification toolset for Simulink and Stateflow models, which generates code in MISRA-C or SPARK. Each tool in the suite offers its own diverse set of enhancements and improvements in the new version 17.1 release.