Polyspace® 静态代码分析产品采用形式化方法证明在所有可能的控制流和数据流下都没有关键运行错误。包括编码规范、安全漏洞、代码指标和数百条其他软件缺陷的检查。
Polyspace Code Prover
无需执行代码即可形式化地证明不存在严重运行时错误
Polyspace Bug Finder
检查编码规则、安全标准、代码指标并找出缺陷
Polyspace for Ada
证明源代码中不存在运行时错误

使用形式化方法为 C/C++ 和 Ada 代码自动执行静态分析
代码质量
无需测试用例或不执行代码的情况下,找出缺陷并形式化证明不存在严重运行时错误。
功能安全
符合 MISRA、ISO 26262、IEC 61508、DO-178 和 FDA 法规的安全标准和文档合规要求。
网络安全
检查软件安全漏洞,及是否符合 CWE、CERT-C、ISO/IEC 17961 和其他标准。