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

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

業界標準には、IEC Certification Kit(for IEC 61508 and ISO 26262) とDO Qualification Kit(for DO-178) によって対応しています。