Abstract-interpretation–based tools such as aiT, StackAnalyzer and Astrée are widely used by key industrial players for validating non-functional safety properties.
aiT was originally designed in the IST project DAEDALUS according to the requirements of Airbus France for validating the timing behavior of critical avionics software, including the flight control software of the A380, the world’s largest passenger aircraft.
Daimler uses aiT in many automotive software projects, including the powertrain control system of the Actros truck.
Vestas uses aiT for static analysis of their wind turbine control software.
OHB uses aiT in the development of software for geostationary communication satellites and satellite navigation.
MTU uses aiT to demonstrate the correctness of control software for emergency power generators in power plants.
NASA used aiT as an industry-standard static analysis tool for demonstrating the absence of timing-related software defects in the 2010 Toyota Unintended Acceleration Investigation.