Polyspace^®代码证明器™是，证明了没有溢出的声静态分析工具，除以零，外的界定数组访问，以及在C和C ++源码其它运行时错误。它产生的结果，而无需执行程序，代码插，或测试用例。Polyspace代码证明器使用基于形式化方法语义分析和抽象解释来验证软件的过程间，控制和数据流的行为。你可以用它来验证手写代码，生成的代码，或两者的组合。每个代码语句是颜色编码，以表明它是否是免费的运行时错误，证明是失败，无法访问，或未经证实的。

Polyspace代码证明器显示范围的变量和函数返回值的信息，并能证明哪些变量超出指定的范围的限制。代码验证结果可以用于跟踪质量指标，并与您的软件质量目标检查一致性。Polyspace代码证明器可以与Eclipse™IDE用来验证您的桌面上的代码。

万博1manbetx对行业标准的支持可通过IEC认证工具包（用于IEC 61508和ISO 26262）和DO资格套件（对于DO-178）。