特許

J-GLOBAL ID：200903018880823959

並行バグ用のエラートレースを生成するシステムおよび方法

発明者： ヴィニート カーロン ,  スリラム サンカラナラヤナン ,  アーティ グプタ
出願人/特許権者： エヌイーシー ラボラトリーズ アメリカ インク
代理人 (3件)： 宮崎 昭夫 ,  石橋 政幸 ,  緒方 雅昭
公報種別：公開公報
出願番号（国際出願番号）：特願2008-291242
公開番号（公開出願番号）：特開2009-123216
出願日： 2008年11月13日
公開日（公表日）： 2009年06月04日
要約：

【課題】同期制約の使用によって得た偽の警告の削減を超える、偽の警告の削減を達成する。【解決手段】プログラム検証のシステムおよび方法は、潜在的誤りに対する警告を捕える並行プログラムの製品トランザクショングラフを生成すること含む。該警告は除去され、並行プログラムの1つまたは2つ以上のデータフロー解析方法を実行することによって導き出される同期プリミティブおよび不変条件からの制約を用いることによって、偽の警告が取り除かれる。データフロー解析方法が経費の順に適用される。具体的な実行トレースが、モデル検査を用いて残存する警告のために生成される。【選択図】図1

請求項（抜粋）：

プロダクトコントロールグラフ上の同期プリミティブによる制約を使用して、静的に到達不可能なノードを取り除くことと、 前記プロダクトコントロールグラフ上で静的プログラム解析を行い正常な不変条件を導き出すことと、 前記の導き出された不変条件を使用して静的に到達不可能なノードをさらに取り除くことと、 次の解析または検証のために、結果として得られたプロダクトコントロールグラフを用いて正当性の違反を検出することと、 を有する、並行プログラムの検証方法。

IPC (2件)：

G06F 11/36 ,  G06F 11/28

FI (2件)：

G06F9/06 620M ,  G06F11/28 B

Fターム (4件)：

5B042HH10 ,  5B042HH30 ,  5B176EC02 ,  5B176EC04

引用特許：

審査官引用 (1件)

• マルチスレッド化されたプログラムにおける潜在的な競合を検出するための方法およびシステム
  公報種別：公開公報   出願番号：特願2005-086776   出願人：マイクロソフトコーポレーション

引用文献：

審査官引用 (2件)

• Fast and Accurate Static Data-Race Detection for Concurrent Programs
• Combining Static Analysis and Model Checking for Software Analysis