Polyspace

Polyspace^® 静态代码分析产品采用形式化方法证明在所有可能的控制流和数据流下都没有关键运行错误。包括编码规范、安全漏洞、代码指标和数百条其他软件缺陷的检查。

无需执行代码即可形式化地证明不存在严重运行时错误

检查编码规则、安全标准、代码指标并找出缺陷

证明源代码中不存在运行时错误

使用形式化方法为 C/C++ 和 Ada 代码自动执行静态分析

无需测试用例或不执行代码的情况下，找出缺陷并形式化证明不存在严重运行时错误。

符合 MISRA、ISO 26262、IEC 61508、DO-178 和 FDA 法规的安全标准和文档合规要求。

检查软件安全漏洞，及是否符合 CWE、CERT-C、ISO/IEC 17961 和其他标准。

日产

Polyspace 不但能够找出会造成运行时错误的操作，还能识别那些无论在何种运行条件下永远都不会出错的操作。

Alenia Aermacchi

Polyspace 静态分析工具会检查代码中是否存在运行时错误，确保符合 MISRA 编码标准，并创建用于 DO-178 合规审定的材料。

Miracor

Polyspace 助力 Miracor 向监管部门（如FDA）展示其代码质量和正确性，以证明其设备安全可靠。