|
|
CompCert - formally verified optimizing C compiler What is CompCert?
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, x86, and RISC-V architectures.
What sets CompCert apart?
... |
|
|
|
Astrée Sound Static code Analyzer Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behavior in safety-critical software written or generated in C. It takes Static analysys one step further by doing a Formal Verification of the code by using the mathematical methodology of Abstract Interpretation. As a result the verification can guarantee there are no run- ... |
|
|
|
StackAnalyzer Stack overflow is a thing of the past StackAnalyzer automatically determines the worst-case stack usage of the tasks in your application. It lets you find any stack overflows, or formally prove the absence thereof.
Call graph with stack usage and worst-case path
Tabular and chart summaries of the analysis results
Features
Detailed and precise informa ... |
|
|
|
AiT - Worst Case Execution Time The industry standard for static timing analysis aiT WCET Analyzers statically compute tight bounds for the worst-case execution time (WCET) of tasks in real-time systems. They directly analyze binary executables and take the intrinsic cache and pipeline behavior into account.
The challenge In real-time systems, timely task completion is of the essence. ... |
|
|
|
TimeWeaver Hybrid worst-case timing analysis TimeWeaver combines static path analysis with timing measurements to provide worst-case execution time estimates.
The tool estimates the worst-case execution time (WCET) of tasks based on the execution time of trace segments obtained from real-time instruction-level tracing. The computed time bounds are valuable for ... |
|
|
|
TimingProfiler Predict timing behavior during code development TimingProfiler helps you identify application parts that cause unsatisfactory execution times. It delivers results as soon as there is compiled code, and thus can be used very early in the development process, when measurements on physical hardware are costly or plain impossible.
This makes TimingProfiler ideally suited for constantly moni ... |
|
|
|
Tool Qualification Package Qualification support Your usage of our tools can be qualified according to ISO 26262, DO-178B/C, IEC-61508, and other safety standards. The qualification process can be automated to a large extent using our Qualification Support Kits. Additionally, our Qualification Software Life Cycle Data Reports provide details about our own development processes.
Qualification Suppor ... |
|