形式検証ツール SPARK Pro

【SPARK Pro】は、形式検証と静的検証が統合されたツール・スイート。データフロー解析機能により、非初期化変数参照など不確実性や不正な動作の原因となるエラーを検出。インフォメーションフロー解析機能にて、プログラムを解析して指定されたデータの依存関係を検証する。そのほか、ゼロ除算、数値オーバーフロー、バッファオーバーフロー、配列の範囲外インデックスなどの実行時例外を検出。セーフティやセキュリティプロパティをcontract(事前、事後条件)で記述し検証が可能。