CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical
and mission-critical software written in C and meeting high levels of assurance. It accepts most of
the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM,
PowerPC, and x86 architectures.
TimingProfiler helps developers identify application parts that are causing unsatisfactory execution times.
It is ideally suited for constantly monitoring timing behavior during software development and in modelbased
development environments. TimingProfiler delivers results as soon as there is compiled code. It can
be used early in the process when measurements on physical hardware are costly or not even possible.
Why do you need StackAnalyzer?
Stack memory has to be allocated statically by the programmer. Underestimating stack usage can lead to serious
errors due to . Overestimating stack overflows stack usage means a waste of memory resources.
· StackAnalyzer provides automatic tool support to calculate the stack usage of your application. The analysis
results are valid for all inputs and each task execution.
· StackAnalyzer analyzes the binary executable and does not rely on debug information, nor on instrumentation.
· Inline assembly code and library function calls are taken into account.
· Recursions and function pointers are taken into account.
· Automatic visualization of call /control-flow graphs with stack usage.
· Current safety standards (DO-178B/C, ISO-26262, IEC-61508, EN-50128, etc.) require to ensure that no stack
overflows can occur. With StackAnalyzer you can prove the absence of stack overflows. AbsInt's Qualification
Support Kits enable a tool qualification up to the highest criticality levels.
Astrée is a parametric static analyzer designed to prove the absence of runtime errors and
data races in software programs written in C. Astrée is parameterizable and can be specialized
to the program under analysis – key features to enable high analysis precision.
Astrée is developed and distributed by AbsInt, under license from the CNRS/ENS. It has been
successfully used on safety-critical software projects from various industry sectors, including
aerospace, automotive, and nuclear energy.
aiT Worst-Case Execution Time Analyzer
Timing Validation for Real-Time Systems
aiT WCET Analyzer computes for the worst-case execution time of tasks
tight bounds in safety-critical systems. These bounds are safe, i.e.
they are valid for any input scenario and each task execution. aiT is
based on statically analyzing a task's intrinsic cache and pipeline
behavior, thus enabling the development of complex hard real-time
systems on state-of-the-art hardware.