Unique tools and services for static analysis
and formal verification of safety-critical software.

aiT computes safe and tight upper bounds for the worst-case execu­tion time of tasks in bina­ry execut­ables, taking into account the cache and pipe­line behavior of the processor in question. TimeWeaver combines static analyses with non-intrusive tracing. And TimingProfiler lets you moni­tor timing behavior at early stages of software devel­opment.

StackAnalyzer determines the worst-case stack usage of tasks in embed­ded applications. 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 ISO 26262, DO-178B, IEC 61508, and other safety standards.

Astrée formally proves the absence of runtime errors and invalid con­current behavior in C and C++ appli­ca­tions. It is sound, very fast, and excep­tionally pre­cise. It can verify MISRA compilance, check code metrics, and run custom signal-flow, component-interference, and cyber­security analyses. Quali­fi­cation for ISO 26262 and DO-178C level A is supported. Jenkins and TargetLink plugins are available.

RuleChecker checks your C or C++ code for compliance with MISRA, CWE, AUTOSAR, and other coding guidelines, including custom rules of your own. It also compiles code metrics and supports easy quali­fi­cation for ISO 26262, DO-178B/C, and other safety standards. Plugins for TargetLink, Eclipse, µVision, and Jenkins 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 two decades now, 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 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 auto­motive software projects, including the powertrain control system of the Actros truck.

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.

Continental has been relying on our stack-analysis service for years to avoid stack overflows in their airbag control systems.

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.

Since 2003, we’ve partnered with the German Aero­space Center on eight dif­fe­rent mid-term research projects, one of them cur­rently ongoing.

Thales Alenia Space have been our partners on five different EU research projects since 2009, among other things using EnergyAnalyzer to estimate the energy consumption of satellite communications software.

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

Framatome 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.

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.

Since 2000, the French Commission for Atomic Energy and Alternative Energies has partnered with us on eight different research projects of the European Union, one of them cur­rently ongoing.

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.