特許

J-GLOBAL ID：200903090684208831

定義集合解析方法

発明者： ロバート ポール カーシャン ,  ケダール シャラッドチャンドラ
出願人/特許権者： ルーセント テクノロジーズ インコーポレイテッド
代理人 (1件)： 三俣 弘文
公報種別：公開公報
出願番号（国際出願番号）：特願2000-199730
公開番号（公開出願番号）：特開2001-056828
出願日： 2000年06月30日
公開日（公表日）： 2001年02月27日
要約：

【要約】【課題】 簡単な、非計算的な構成性の定義(Constructivity-SAT)と、新しい定式化に基づく、任意の有限型の変数に対して実装が簡単な記号アルゴリズムとによって、回路定義を改善する。【解決手段】 簡単な変換によって、値⊥(「ボトム」と読む)で拡張された変数型に関する、定義から導出された方程式集合の充足可能性として、構成性を再定式化することができることが示される。この定式化は、非計算的であり、任意の有限型の変数に容易に拡張可能である。また、この定式化は、同様にして、添字つき変数の定義も扱う。この構成性チェックはCOSPANで実装された。COSPANは、市販のFormalCheck検証ツールのための検証エンジンである。この実装は簡単であり、経験によれば、通常、無視しうるオーバーヘッドしか受けない。

請求項（抜粋）：

巡回動作に対して定義集合を解析する方法において、前記定義集合内の変数のうちの少なくとも一部の変数を、⊥値を含む変数型に変換することにより、修正定義集合を形成するステップと、前記修正定義集合の解が、値が⊥の変数を含むかどうかを確認するステップとを有することを特徴とする定義集合解析方法。

IPC (2件)：

G06F 17/50 664 ,  G06F 17/50

FI (2件)：

G06F 17/50 664 A ,  G06F 17/50 664 Z

引用特許：

審査官引用 (1件)

• 静的半順序換算
  公報種別：公開公報   出願番号：特願平10-313128   出願人：ルーセントテクノロジーズインコーポレーテッド