Industry perspective

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 re­quirements of Airbus France for validating the timing behavior of crit­i­cal avionics software, including the flight control software of the A380, the world’s largest passenger aircraft.

Daimler uses aiT in many auto­motive software projects, including the powertrain control system of the new 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 cor­rectness 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 Accel­eration Investigation.