aiT automatically computes safe bounds for the worst-case execution time of tasks in binary executables, taking into account the cache and pipeline behavior of the processor in question. TimeWeaver combines static analyses with measurements obtained from hardware traces. And TimingProfiler lets you monitor timing behavior at early stages of software development.
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 ISO 26262, DO-178B, IEC 61508, and other safety standards.
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.
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.
For two decades now, Airbus France has been using our tools in the development of safety-critical avionics software for several airplane types, including the flight control software of the A380, the world’s largest passenger aircraft.
Honda used our tools in developing the FADEC software of a turbofan engine.
The Technical University of Munich is using our tools in the development, testing and optimization of flight control and navigation algorithms.
Daimler has been using our tools in many automotive software projects, including the powertrain control system of the new Actros truck.
NASA used our timing-analysis tool for demonstrating the absence of timing-related software defects in the 2010 Toyota investigation.
Continental, one of the world’s largest automotive suppliers, has been relying on our stack-analysis service for years to avoid stack overflows in their airbag control systems.
Bosch Automotive Steering replaced their legacy tools with Astrée and RuleChecker, resulting in significant savings thanks to faster analyses, higher accuracy, and lower licensing costs.
OHB uses our tools in the development of onboard software essential for mission success of the SmallGEO platform for geostationary communication satellites and the GALILEO FOC+++ platform for satellite navigation.
ESA used our runtime-error analyzer to prove the absence of runtime errors in the automatic docking software of the Jules Verne Automated Transfer Vehicle, enabling it to transport payloads to the International Space Station.
Framatome employs our runtime error analysis and stack analysis tools to verify their safety-critical TELEPERM XS platform that is used for engineering, testing, operating and troubleshooting nuclear reactors.
MTU uses our tools for verified compilation and static program analysis to ensure the correctness of control software for emergency power generators in power plants.
As a leading provider of embedded wireless communication and positioning solutions, u‑blox is using our tools to avoid stack overflow at compile time and to increase the reliability and quality of their controlling software.
Siemens used our expertise to drastically reduce the size of their mobile-phone applications, allowing 25% more functionality to be packed into the flash memory of millions of mobile phones worldwide.