NECおよび松下電器産業は，「モデル検査（model checking）」と呼ぶ技術を応用して，メモリ・リークなどC言語プログラムの実行時エラーを検出する技術を，それぞれ開発した。一般にメモリ・リークなどの実行時エラーは，プログラムを実際に実行するテスト，特に開発工程後半のシステム・テスト時に検出することが多いが，今回の技術は一種の静的検証ツールとして利用できるため，ソース・コードが出来上がった直後など，開発工程のより早い段階でこれらの不具合を検出しやすくなる利点がある。

　NECは今回の技術を用いて社内向けの検証サービスを既に実施しており，数人の検証専門技術者が180万行のソース・コードから37件のバグを検出するなどの効果を上げた。今後，ツールの外販も計画している。松下電器産業は主に，社内向けに運用していく計画だ。