Fast and sound runtime error analysis

Astrée is a static program analyzer that proves the absence of run­time errors and invalid con­current behavior in safety-critical appli­cations written or gen­er­ated in C.

Astrée screenshot
Astrée screenshot

Astrée analyzes structured C programs with complex memory usages or even dynamic memory allocation, but without recursion. This targets embedded applications as found in earth trans­por­tation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular syn­chro­nous control/command such as electric flight control.

Astrée is sound — that is, if no errors are signaled, the absence of errors has been proved.

Which runtime properties are analyzed by Astrée?

Astrée analyzes whether the C programming language is used correctly and whether there can be any run­time errors during any execution in any environment. This covers any use of C that, according to the C99 standard, has undefined behavior or violates hardware-specific aspects.

Additionally, Astrée reports invalid concurrent behavior, violations of user-specified programming guidelines, and various program properties relevant for functional safety.

Astrée detects any:

Astrée is sound for floating-point computations and handles them precisely and safely. All possible rounding errors, and their cumu­lative effects, are taken into account. The same is true for −∞, +∞ and NaN values and their effects through arithmetic calculations and comparisons.

MISRA rule checker

Astrée is able to check for MISRA coding rules, compute code metrics (com­ment den­sity, cyclomatic complexity…), and check metric thresholds. The integrated rule checker supports both MISRA 2004 and MISRA 2012. It is highly configurable, allowing you to check for individual rules and even specific aspects of certain rules.

Who uses Astrée?

  • Aviation

    In 2003, Astrée proved the ab­sence of any run­time errors in the primary flight-control software of an Airbus model. The sys­tem’s 132,000 lines of C code were ana­lyzed com­pletely automatically in only 80 minutes on a 2.8GHz 32-bit PC using 300MB of memory (and in only 50 min­utes on an AMD Athlon 64 using 580MB of memory). Since then, Airbus France has been using Astrée in the devel­opment of safety-critical software for vari­ous plane series, including the A380.

  • Space flight

    Jules Verne ATVCourtesy of NASA

    In 2008, Astrée proved the absence of any run­time errors in a C ver­sion of the auto­matic docking software of the Jules Verne Automated Transfer Vehicle (ATV), enabling ESA to transport payloads to the Inter­national Space Station. This was the first fully automatic docking maneuver not per­formed by a Rus­sian vessel.

  • Automotive

    The global automotive supplier Helbako in Germany is using Astrée to guar­antee that no run­time errors can occur in their elec­tronic control software and to de­monstrate MISRA compliance of the code.

  • Power plants

    MTU Friedrichshafen uses Astrée to demonstrate the cor­rectness of con­trol software for emer­gency power gene­rators in power plants. The tool in combination with its qualification package is part of the certi­fication process according to the IEC 60880.

  • Ventilation

    A world leader in motors and ventilators for air-conditioning and refrigeration systems, ebm-papst is using Astrée for fully automatic conti­nuous verification of safety-critical interrupt-driven control software for commu­tating high-efficiency EC motors for venti­lator systems.


Tailor it to your own requirements

Astrée offers powerful annotation mechanisms for supplying external knowledge and fine-tuning the ana­lysis precision for individual loops or data structures. Detailed messages and an intui­tive GUI help you understand alarms about potential errors. Actual errors can then be fixed, and in case of a false alarm, the analyzer can be tuned to avoid it. This allows for analyses with very few or even zero false alarms.

The analyzer can also run in batch mode for easy integration into established tool-chains.

Qualification support

We offer special qualification support kits for Astrée that simplify the qualification process for DO-178B level A, ISO 26262, IEC 61508, and other safety standards.

Ten years ahead of competition

Astrée is…

  • Sound

    Most static analyzers do not consider all possible run­time errors. Others specifically focus on the most probable ones.

    As a result, almost all competing tools can only be used for static testing (i.e. finding out the most frequently occuring bugs), but never for verification (i.e. proving the absence of any run­time errors).

    In contrast, Astrée is sound. It always exhaustively considers all pos­sible run­time errors. It will never omit pointing out a potential run­time error. This is crucial for verification of safety-critical software. At the same time, Astrée is capable of producing exactly zero false alarms.

  • Automatic

    Certain static analyzers (e.g. those relying on theorem provers) require programs to be annotated with lots of inductive invariants.

    Astrée usually requires very few annotations. It can even run completely automatically on certain types of programs, without relying on any help from the user.

    Many analyzers cannot be scripted at all. Some of those that can, won’t let you access their analysis results outside of their proprietary viewer. This actively prevents you from automating the analysis, e.g. as part of your nightly build process.

    In contrast, Astrée offers you complete access to the analysis engine in batch mode, and lets you freely export the analysis results and further process them in any way you choose, no strings attached.

  • Fast

    Many static analyzers have high computational costs (typically sever­al hours of compu­tation per 10,000 lines of code). Others terminate out of memory, or may not terminate at all.

    In contrast, Astrée is efficient and easily scales up to real-world pro­grams in industrial practice. For example, Astrée needed only 80 min­utes on a 2.8GHz PC to ana­lyze the flight-control software of an Airbus model, which comprised 132,000 lines of C code. Since 2005, Astrée can run on multi­core parallel or distri­buted machines, providing for even faster analysis.

  • Domain-aware

    General-purpose static analyzers aim at analyzing any application written in a given pro­gram­ming language. They can rely on language related properties to find potential run­time errors. Specialized static analyzers put additional restrictions on the app­lications so as to be able to take specific program structures into account.

    In contrast, Astrée is domain-aware. It thus knows facts about ap­pli­ca­tion domains that are indispensable to make sophisticated proofs. For example, for control/command programs, Astrée takes the logic and functional properties of control/command theory into account.

  • Parametric

    In static program analysis, there is always a trade-off between analysis precision and analysis cost. Analyzers that are precise are usually also very slow, while fast analyzers usually lack precision.

    In contrast, Astrée is parametric, which means that it allows you to freely trade speed for precision and vice versa. The level of abstraction used for analysis can be easily tailored to your very own requirements.

  • Modular

    Astrée consists of several modules (so-called abstract domains). These modules can be assembled and parameterized to build application-specific analyzers that are fully adapted to a particular ap­plication domain or specific end-user requirements.

    In case of false alarms, Astrée can be easily extended by intro­duc­ing additional modules that enhance the precision of the analysis.

  • Precise

    General-purpose static analyzers usually suffer from low precision in terms of false alarms, i.e. spurious warnings about errors that can actu­ally never occur at run­time. The ratio of false alarms to the number of basic C operations typically ranges between 10% and 20%.

    Specialized analyzers achieve a better precision of 10% or less. How­ever, even a very high selectivity rate of only 1 false alarm for every 100 operations is usually unacceptable for large real-world appli­cations. For example, on a program with 100,000 operations, a selec­tivity rate of only 1% yields 1000 false alarms.

    In contrast, thanks to its modularity and domain-awareness, Astrée can be made exceptionally precise, often to the point of pro­ducing exactly zero false alarms. This has been repeatedly proven in indus­tri­al practice, e.g. when analyzing primary flight-control software for Airbus.

  • Up-to-date

    Astrée not only builds upon decades of research in static program analysis, but also incorporates the latest ongoing research, always staying well ahead of any competition.

    Major new releases are published twice a year, intermediate releases more often still. If you have a feature request, let us know at support@absint.com.


Free trial

Request your free trial package today.