Tel. +31­ 345 545535
Coming soon...
Who we work with
What's going on
Something to read
Who we are
Where we are
You are on the following page: Products > Safety Critical & Certified Systems > Formal Verification English | Nederlands

Formal Verification

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 ac­cepts 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 run­time errors and invalid con­current behavior in safety-critical software written or gen­er­ated 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- ...
Stack overflow is a thing of the past
StackAnalyzer automatically determines the worst-case stack usage of the tasks in your appli­cation. 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. ...
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 exe­cution time of trace segments obtained from real-time instruction-level tracing. The computed time bounds are valuable for ...
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 measure­ments 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 qualifi­cation process can be automated to a large extent using our Qualification Support Kits. Addition­ally, our Qualification Software Life Cycle Data Reports provide details about our own devel­op­ment processes. Qualification Suppor ...


INDES-IDS BV offers solutions for Embedded Software Development as well as for the Telecommunication NEMS and Service Providers. In these markets we offer products of either the market leader or the innovation leaders. Our goal is to assist you to get to the market sooner by offering a combination of products, knowledge and services.