Unique tools and services for the development,
analysis, and certification of safety-critical software.

aiT automatically computes tight upper bounds for the worst-case execu­tion time of tasks in real-time systems. It direct­ly analyzes bina­ry execut­ables and takes cache and pipe­line behavior into account. No testing or measuring is necessary, the analysis results hold for all in­puts and execu­tion scena­rios. Special kits simpli­fy the quali­fica­tion for DO-178C, ISO 26262, and other safety stan­dards.

StackAnalyzer automatically determines the worst-case stack usage of the tasks in embed­ded appli�cations. It directly ana­lyzes binary execut­ables and considers all possible execution scenarios. Tight inte­gration with TargetLink and SCADE is avail­able, as well as qualifi­cation kits for standards such as ISO 26262, DO-178B, and IEC 61508.

Astrée automatically proves the absence of runtime errors and invalid con­ï¿½current behavior in C appli­ca­tions. It is sound for floating-point compu­tations, very fast, and excep­tionally precise. The analyzer also checks for MISRA coding rules and supports quali­fi­cation for ISO 26262, DO-178C level A, and other safety standards. Jenkins and Eclipse plugins are available.

CompCert is a formally verified optimizing C com­piler for safety-critical and mission-critical soft­ware. Unlike any other produc­tion compiler, it is mathe­ma­tic­ally proven to be exempt from mis­compila­tion issues. Such confi­dence in the correct­ness of the compila­tion process is un­prece­dent­ed and helps meet the highest levels of soft­ware assurance.

For over a decade, Airbus France has been using our tools in the develop­ment of safety-critical avionics software for sever­al air­plane types, including the flight control soft­ware of the A380, the world’s largest passenger air­craft.

Honda has been using 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 auto­motive software projects, including the powertrain control system of the new Actros truck.

NASA used our timing-analysis tool for demonstra­ting the absence of timing-related software defects in the 2010 Toyota investi­gation.

OHB uses our tools in the develop­ment of onboard soft­ware essential for mission success of the SmallGEO platform for geo­stationary commu­ni­cation satellites and the GALILEO FOC+++ platform for satellite navi­gation.

ESA used our runtime-error analyzer to prove the absence of runtime errors in the auto­matic docking software of the Jules Verne Automated Transfer Vehicle, enabling it to transport pay­loads to the Inter­national Space Station.

Vestas uses our tools to prevent stack overflow and to verify the timing behavior of their wind turbine control software.

AREVA employs our runtime error analysis and stack analysis tools to verify their safety-critical TELEPERM XS platform that is used for engineer­ing, testing, operating and trouble­shooting nuclear reactors.

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 control­ling 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.