Polyspace Code Prover

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

Polyspace Code Prover では、変数および関数の戻り値の範囲情報も表示され、指定された範囲限界値を超えた変数を証明できます。結果はダッシュボードにパブリッシュできるため、品質メトリクスを追跡して、ソフトウェア品質目標に確実に準拠させることができます。

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