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

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

可通过IEC认证套件(适用于IEC 61508和ISO 26262)和DO资格认证套件(适用于DO-178)支持行业标准。