Polyspace Code Prover

ソフトウェアにランタイム エラーがないことを証明

Polyspace Code Prover™ は、C および C++ ソース コード内にオーバーフロー、ゼロ除算、範囲外の配列へのアクセス、その他の特定のランタイム エラーがないことを証明します。結果の生成には、プログラムの実行や、コードの計測、テスト ケースは必要ありません。Polyspace Code Prover は静的解析と形式手法に基づいた抽象解釈を使用します。手書きのコード、生成されたコード、またはこの 2 つの混合コードに使用することができます。ソースコードに対し、ランタイム エラーは発生しない(常に信頼できる)、ランタイムエラーは常に発生する、到達不能な処理がある、ランタイムエラーの可能性がある(未証明)を示すように色分け表示されます。

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

業界標準には、IEC Certification Kit (IEC 61508 および ISO 26262 用) および DO Qualification Kit (DO-178 用) に対応しています。Ada 言語 にも対応しています。

モデルとコードのテスト検証

Web セミナーを表示する

評価版 Polyspace Code Prover

評価版ソフトウェアを入手する

製品評価版の入手または製品の購入

Jay Abraham

新着情報

Jay Abraham、 Polyspace Code Prover 技術エキスパート