Astrée (static analysis)

Astrée is a static analyzer based on abstract interpretation. It analyzes programs written in the C programming language and outputs an exhaustive list of possible runtime errors and assertion violations.

The tool is tailored towards safety-critical embedded code: source programs are assumed not to contain dynamic allocation (malloc); specific analysis techniques are used for common control theory constructs (filters, rate limiters...) and floating-point numbers.

Astrée was developed in Patrick Cousot's group at École Normale Supérieure, a joint group with CNRS, and is marketed by AbsInt GmbH. It is used in the Defense/Aerospace, Industrial Control, Electronic, and Automotive industries. One of the main industrial users is Airbus.

Astrée is a commercial product available from AbsInt Angewandte Informatik.

...
Wikipedia