Static analyses and formal verification
for ARM applications

Our tools offer a vast variety of static analyses for the development, debugging, optimization, and certification of safety-critical and mission-critical ARM applications.

Qualification Support Kits are available to help you with the qualification for ISO 26262, DO-178B/C, IEC-61508, and other safety standards.

You can also commission us with the analysis of your code. Any of the analyses listed below can be carried out as a service according to your requirements.





CC++
Runtime error analysis Astrée Astrée
Data race analysis Astrée Astrée
Non-interference analysis Astrée Astrée
Taint analysis Astrée Astrée
Signal-flow analysis Astrée Astrée
Data-flow analysis Astrée Astrée
Control-flow analysis Astrée Astrée
Control-coupling analysis Astrée Astrée
Component-interference analysis Astrée Astrée
Cybersecurity analyses Astrée Astrée
Spectre vulnerability detection Astrée Astrée
Rule checking (MISRA) Astrée, RuleChecker Astrée, RuleChecker
Rule checking (other) Astrée, RuleChecker Astrée, RuleChecker
Rule checking (custom) Astrée, RuleChecker Astrée, RuleChecker
Code metrics (HIS) Astrée Astrée
Verified compilation CompCert
Control flow visualization Astrée Astrée
Dead code recognition Astrée Astrée
Dead code elimination CompCert
Postpass validation Valex
compiled C compiled C++ compiled Ada
Static WCET analysis aiT aiT aiT
Hybrid WCET analysis TimeWeaver TimeWeaver TimeWeaver
Timing profiling TimingProfiler TimingProfiler TimingProfiler
Stack usage analysis StackAnalyzer StackAnalyzer StackAnalyzer
Memory safety analysis ValueAnalyzer ValueAnalyzer ValueAnalyzer
Energy consumption analysis EnergyAnalyzer EnergyAnalyzer EnergyAnalyzer
Control flow visualization all of the above all of the above all of the above
Dead code recognition all of the above all of the above all of the above