Abstract-interpretation–based tools such as StackAnalyzer, aiT and Astrée are widely used by key industrial players for validating non-functional safety properties.