Run-Time Error Analyzer
Astrée - AbsInt Angewandte Informatik GmbH (AbsInt)
Astre analyzes structured C programs with complex memory usages, but without recursion or dynamic memory allocation. This targets embedded applications as found in earth transportation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular synchronous control/command such as electric flight control.