CompCert is a formally verified optimizing C compiler for safety-critical and mission-critical software. Unlike any other production compiler, it is mathematically proven to be exempt from miscompilation issues. Such confidence in the correctness of the compilation process is unprecedented and helps meet the highest levels of software assurance
aiT automatically computes tight upper bounds for the worst-case execution time of tasks in real-time systems. It directly analyzes binary executables and takes cache and pipeline behavior into account. No testing or measuring is necessary, the analysis results hold for all inputs and execution scenarios. Special kits simplify the qualification for DO-178C, ISO 26262, and other safety standards.
StackAnalyzer automatically determines the worst-case stack usage of the tasks in embedded applications. It directly analyzes binary executables and considers all possible execution scenarios. Tight integration with TargetLink and SCADE is available, as well as qualification kits for standards such as ISO 26262, DO-178B, and IEC 61508.
Run Time Error Analysis
Astrée automatically proves the absence of runtime errors and invalid concurrent behavior in C applications. It is sound for floating-point computations, very fast, and exceptionally precise. The analyzer also checks for MISRA coding rules and supports qualification for ISO 26262, DO-178C level A, and other safety standards. Jenkins and Eclipse plugins are available.
Reliability Software from Isograph, UK. Isograph was founded in 1986 and is now one of the world’s leading companies in the development and provision of integrated Reliability, Availability, Maintainability and Safety software products. Isograph software is used in all industries when Reliability, Availability and Safety are paramount. It is also used at universities throughout the world to teach undergraduate and postgraduate courses in engineering.