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

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

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