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

Polyspace代码验证では,変数および関数の戻り値の範囲情報も表示され,指定された範囲限界値を超えた変数を証明できます。検証結果をダッシュボードに公開して品質メトリクスを追跡し,ソフトウェア品質目標に確実に適合することができます。Polyspace代码验证をビルドシステムに統合すると,自動化された検証を実行することができます。

業界標準には,IEC认证工具包(IEC 61508とISO 26262用)と做资格工具包(- 178用)によって対応しています。