Polyspace Code Prover™证明在C和c++源代码中没有溢出、除零、越界数组访问和某些其他运行时错误。它产生的结果不需要程序执行、代码插装或测试用例。Polyspace Code Prover采用静态分析和基于形式化方法的抽象解释。您可以在手写代码、生成代码或两者的组合上使用它。每个操作都用颜色编码，以指示它是否没有运行时错误、已证明失败、不可到达或未证明。

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

通过IEC认证套件(适用于iec61508和iso26262)和DO认证套件(适用于DO-178)，您可以获得对行业标准的支持。