Polyspace Code Prover

Polyspace^® Code Prover™ 可证明 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和某些其他运行时错误。它无需程序执行、代码插桩或测试用例即可生成结果。Polyspace Code Prover 使用基于形式化方法的静态分析和抽象解释。您可以将它应用于手写代码、生成的代码或这两者的组合。每个运算都进行了着色，以指示它是否存在运行时错误、是否已证明失败、是否不可达或是否未经证明。

Polyspace Code Prover 还会显示变量和函数返回值的范围信息，并且可以证明哪些变量超出了指定的范围限制。结果可发布到仪表板上，以跟踪质量度量并确保符合软件质量目标。

通过 IEC Certification Kit (for ISO 26262 and IEC 61508) 和 DO Qualification Kit (for DO-178) 实现对行业标准的支持。