Static analyses and formal verification
for dsPIC applications

Our tools offer a variety of static analyses for the development, debugging, optimization, and certification of safety-critical applications for dsPIC33E.

Qualification Support Kits are available to help you with the qualification for ISO 26262, DO-178B/C, IEC-61508, and other safety standards.

You can also commission us with the analysis of your code. Any of the analyses listed below can be carried out as a service according to your requirements.

C source code
Runtime error analysis Astrée
Data race analysis Astrée
Non-interference analysis Astrée
Taint analysis Astrée
Signal-flow analysis Astrée
Data-flow analysis Astrée
Control-flow analysis Astrée
Control-coupling analysis Astrée
Component-interference analysis Astrée
Cybersecurity analyses Astrée
Rule checking (MISRA) Astrée, RuleChecker
Rule checking (other) Astrée, RuleChecker
Rule checking (custom) Astrée, RuleChecker
Code metrics (HIS) Astrée
Control flow visualization Astrée
Dead code recognition Astrée
compiled C
Timing profiling TimingProfiler
Stack usage analysis StackAnalyzer
Memory safety analysis ValueAnalyzer
Control flow visualization all of the above
Dead code recognition all of the above