Polyspace

Polyspace^® 静态代码分析产品采用形式化方法证明在所有可能的控制流和数据流下都没有关键运行错误。包括编码规范、安全漏洞、代码指标和数百条其他软件缺陷的检查。Polyspace Test™ 为嵌入式系统的 C 和 C++ 代码提供了开发、管理和执行单元与集成测试的工具。

识别编码缺陷，查看静态分析结果，并监控软件质量指标

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

通过在服务器上运行的静态分析识别软件缺陷

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

证明软件中不存在运行时错误

开发、管理和执行嵌入式系统中 C 和 C++ 代码的测试

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

在计算机集群上执行代码验证并发布指标

索取试用版

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

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

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

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

Volvo Cars

借助 Polyspace，我们可以在每次代码合并之前识别并修复关键的运行时错误，从而确保软件的安全性和质量。

Alenia Aermacchi

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

Miracor

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