Formally proves the absence of run­time errors and invalid concurrent behavior in safety-critical software written or generated in C or C++. 

Astrée primarily targets embedded applications, analyzing any structured C/C++ programs, handwritten, or generated, with complex memory usages, dynamic memory allocation, and recursion.