組込みソフトウェアテスト・静的解析ツール部門で注目

Polyspace Code Prover

マスワークス合同会社

C/C++の実行時エラーが無いことを証明する静的解析

MathWorksのC/C++向け静的解析ツール。抽象解釈を使い、プログラムの実行やテストケースなしで、オーバーフロー、ゼロ除算、配列の範囲外アクセスなどの実行時エラーの有無を確かめ、重大な実行時エラーが存在しないことを証明する。タスク間で共有するグローバル変数への同時アクセス、デッドコードや到達できない分岐も検出する。結果はソースコード上に色分けして表示し、変数がとりうる範囲をツールチップで示す。60以上のC/C++コンパイラに対応し、手書きのコードとSimulinkで生成したコードの両方に使える。IEC 61508とISO 26262に沿った使用についてTÜV SÜDの認証を得ている。CI向けのPolyspace Code Prover Serverもある。