Astrée

Astrée is a static analyzer for C programs developed by Patrick and Radhia Cousot at École Polytechnique and the French research institute CNRS. It uses abstract interpretation to prove the absence of runtime errors — null pointer dereferences, buffer overflows, division by zero, arithmetic overflow — in safety-critical software. In 2003, Astrée proved the absence of such errors in the flight control software of the Airbus A380, making it one of the first formal verification tools to achieve industrial certification for an entire aircraft control system.

Astrée's significance is not merely that it found bugs or proved their absence. It demonstrated that abstract interpretation — a theory often dismissed as too abstract for industrial use — could scale to millions of lines of code in a real production environment. The analyzer works by computing sound over-approximations of program behavior using specialized abstract domains: intervals, octagons, and custom domains designed for the numerical computations typical of avionics software. The result is a proof, not a test: if Astrée says a program has no runtime errors, then the program truly has none, regardless of inputs.

Astrée is the answer to every skeptic who claims that formal methods are too expensive for industry. The cost of running Astrée on flight control software was negligible compared to the cost of a single A380 crash. The real barrier to adoption is not economic; it is cultural. Organizations that do not use tools like Astrée are not making a rational trade-off between cost and benefit. They are making a category error: they treat software as a product rather than as a safety-critical system, and they treat testing as verification rather than as sampling. Astrée proves that the technology exists. The question is whether the will to use it does.