For all your static analysis needs

Am486

ARM

AURIX

C16x

C28x

C33

ColdFire

dsPIC

ERC32

FR81S

HCS12

i386DX

LEON2

LEON3

LEON4

M68k

MCS251

MCS51

MIPS32

MSP430(x)

Nios II

PowerPC (32-bit)

PowerPC (64-bit)

RH850

RISC-V

RL78

RX

S12Z

ST10

STAR12

SuperH

TriCore

V850

x86 (16-bit)

x86 (32-bit)

x86 (64-bit)

ARC

  • Stack usage analysis
  • Memory safety analysis
  • Available till 2015
  • Get in touch

H8

  • Stack usage analysis
  • Memory safety analysis
  • Available till 2013
  • Qualification Support Kit
  • Get in touch

HC11

  • Static WCET analysis
  • Stack usage analysis
  • Memory safety analysis
  • Available till 2015
  • Get in touch

Kalray

  • Static WCET analysis
  • Developed for the EU project ASSUME
  • Available at our discretion
  • Get in touch

M32

  • Static WCET analysis
  • Stack usage analysis
  • Memory safety analysis
  • Available till 2011
  • Get in touch

MicroBlaze

  • Static WCET analysis
  • Developed for the EU project CERTAINTY
  • Available at our discretion
  • Get in touch

PCP2

Xentium

  • Static WCET analysis
  • Developed for the EU project ARGO
  • Available at our discretion
  • Get in touch

Language support

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 compiled PL/I
Static WCET analysis aiT aiT aiT aiT
Hybrid WCET analysis TimeWeaver TimeWeaver TimeWeaver —
Timing profiling TimingProfiler TimingProfiler TimingProfiler TimingProfiler
Stack usage analysis StackAnalyzer StackAnalyzer StackAnalyzer StackAnalyzer
Memory safety analysis ValueAnalyzer ValueAnalyzer ValueAnalyzer ValueAnalyzer
Energy consumption analysis EnergyAnalyzer EnergyAnalyzer EnergyAnalyzer —
Control flow visualization all of the above 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 all of the above