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