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 Sytems > Formal Verification Nederlands | French

Formal Verification

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- ...
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? ...


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.