Polyspace^®代码验证™は安定性の高い静的解析ツールで,Cおよびc++ソースコード内のオーバーフロー,ゼロ除算,配列の範囲外へのアクセスおよびその他のランタイムエラーの有無が証明されます。プログラムの実行，コ，ド計測またはテストケ，スを必要とすることなく，結果が生成されます。多空间代码证明では,セマンティクスの解析および形式的手法に基づく抽象的な解釈が使用され,ソフトウェアの手続き間のフロー,制御フロー,およびデータフローの動作が検証されます。また，手書きのコ，ド，生成されたコ，ドまたはその2の組み合わせの検証に使用できます。各コードステートメントは色分けされ,ランタイムエラーなし,エラーと証明,到達不能,または未証明のいずれかであることが示されます。

多空间代码证明では，変数および関数の戻り値の範囲情報が表示され，指定された範囲限界値を超えた変数を証明できます。コ，ド検証の結果を使用して品質メトリクスを追跡し，ソフトウェア品質目標との一致をチェックできます。多空间代码证明はEclipse™IDEと共に使用して，デスクトップ上でコ，ドを検証できます。

業界標準には，IEC认证套件(适用于iec61508及iso26262)とDO资格套件(适用于DO-178)によって対応しています。