(57)【要約】【課題】経路に依存しない解析を使用する経路に依存する解析のための抽象的解釈を使用して、プログラムを静的に分析する。【解決手段】実行不可能な経路検出のためのシステム及び方法は、プログラムの性質を証明するためのプログラムに静的解析を行うことを含んでいる。性質が証明されなければ、経路に依存しない抽象的解釈を行うことによって、プログラム内の実行不可能な経路が決定される。このような実行不可能な経路についての情報は、経路に依存しないプログラム解析において経路依存性の効果を実現するために使用される。【選択図】図１
2009176282.tif 000002
【特許請求の範囲】
【請求項１】
プログラム内の実行不可能な経路を検出する方法であって、
前記プログラムの性質を証明するために、前記プログラムに静的解析を行うことと、
前記性質が証明されなければ、経路に依存しない抽象的解釈を行うことにより、前記プログラム内の実行不可能な経路を決定することとを含む、プログラム内の実行不可能な経路を検出する方法。
【請求項２】
前記実行不可能な経路を前記プログラムから除外するために、構文上の言語改良を実行し、後続の解析のために改良されたプログラムを結果として生ずることを、さらに含む請求項１記載の方法。
【請求項３】
前記プログラムの経路依存性を得るために、実行不可能な経路の除外の後に、前記改良されたプログラムの経路に依存しない解析を使用することを、さらに含む請求項２記載の方法。
【請求項４】
実行不可能な経路を決定することは、前記プログラムの具体的な実行では行えない経路を推測するために、適切な抽象ドメインを使用して、一連の経路に依存しない順方向及び逆方向の伝搬を行うことを含む請求項１記載の方法。
【請求項５】
プログラム・ポイントにおいて到達可能なプログラム状態に対応するアサーションを決定することと、
実行不可能な経路を決定するために、その連合が論理的に偽である前記アサーションの部分集合を生成することとを、さらに含む請求項４記載の方法。
【請求項６】
その連合が論理的に偽であるアサーションの部分集合を生成するために、ブーリアン満足化可能性ソルバー及び理論満足化可能性チェッカーが組み合わせて使用される、請求項５記載の方法。
【請求項７】
その連合が論理的に偽であるアサーションのより小さい部分集合を学習するために、前記理論満足化可能性ソルバーからの非満足化可能性の証明が使用される請求項６記載の方法。
【請求項８】
それらの連合が論理的に偽であるか否かを決定するために、前記プログラムの連続した経路部分に対応するアサーションの部分集合がチェックされる請求項６記載の方法。
【請求項９】
前記実行不可能な経路をデータベースに蓄積することを、さらに含む請求項１記載の方法。
【請求項１０】
プログラムの実行不可能な経路検出の方法であって、
前記プログラムの性質を証明するために、前記プログラムに静的解析を行うことと、
前記性質が証明されなければ、前記プログラムの具体的な実行では行えない経路を推測するために抽象ドメインを使用して、経路に依存しない抽象インタプリター内で一連の経路に依存しない順方向及び逆方向の伝搬を行うことによって、前記プログラム内の実行不可能な経路を決定することと、
前記プログラムから前記実行不可能な経路を除外するために、構文上の言語改良を行うことを含む、プログラムの実行不可能な経路検出の方法。
【請求項１１】
構文上の言語改良を実行することは、後続の解析のために改良されたプログラムを結果として生じ、また、前記プログラムの経路依存性を得るために、実行不可能な経路の除外の後に、前記改良されたプログラムの経路に依存しない解析を使用することを、さらに含む請求項１０記載の方法。
【請求項１２】
プログラム・ポイントにおいて到達可能なプログラム状態に対応するアサーションを決定することと、実行不可能な経路を決定するために、その連合が論理的に偽である前記アサーションの部分集合を生成することを、さらに含む請求項１０記載の方法。
【請求項１３】
その連合が論理的に偽であるアサーションの部分集合を生成するために、ブーリアン満足化可能性ソルバー及び理論満足化可能性チェッカーが組み合わせて使用される、請求項１２記載の方法。
【請求項１４】
その連合が論理的に偽であるアサーションのより小さい部分集合を学習するために、前記理論満足化可能性ソルバーからの非満足化可能性の証明が使用される請求項１３記載の方法。
【請求項１５】
それらの連合が論理的に偽であるか否かを決定するために、前記プログラムの連続した経路部分に対応するアサーションの部分集合がチェックされる請求項１２記載の方法。
【請求項１６】
前記実行不可能な経路をデータベースに蓄積することを、さらに含む請求項１０記載の方法。
【請求項１７】
実行不可能な経路検出のためのシステムであって、
プログラムの性質を証明するプログラムにおいて静的解析を行うように構成された抽象的解釈エンジンであって、前記エンジンは、プログラム・ポイントにおいて到達可能なプログラム状態に対応するアサーションを決定するために、抽象ドメインを使用して、一連の経路に依存しない順方向及び逆方向の伝搬により、経路に依存しない抽象的解釈を行うように構成された、プログラムの性質を証明するプログラムにおいて静的解析を行うように構成された抽象的解釈エンジンと、
前記プログラム内の実行不可能な経路を決定するために、その連合が論理的に偽であるアサーションの部分集合を生成するために、組み合わせて使用される満足化可能性ソルバー及び理論満足化可能性チェッカーとを有する、実行不可能な経路検出のためのシステム。
【請求項１８】
前記改良されたプログラムでの経路に依存しない解析が、実行不可能な経路の除去の後に、前記プログラムでの経路依存性を得るために実行されるように、前記実行不可能な経路を前記プログラムから除外し、後続の解析のために改良されたプログラムを結果として生ずる構文上の言語改良を、さらに含む請求項１７記載のシステム。
【請求項１９】
前記実行不可能な経路を蓄積するデータベースをさらに含む請求項１７記載のシステム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータ検証に関し、特に、経路に依存しない解析を使用する経路に依存する解析のための抽象的解釈を使用して、プログラムを静的に分析するためのシステム及び方法に関する。
【背景技術】
【０００２】
プログラム解析には、経路依存性を組み込む３つの重要なカテゴリーがある。（ａ）解析において異なるプログラム・ポイントから、寄与を選択的に組み合わせあるいは分離して、経路依存解析を実行する。（ｂ）分離的な不変量を直接追跡するために、抽象ドメインの分離的完了を行う。しかし、この処理は費用が掛かり、完全に実用的ではない。（ｃ）ループを効率的にさらにアンロールするために使用した反復方式を変更することによるか、あるいは、不動点誘導抽象化改良方式を使用するか、のいずれかによって、繰り返し抽象化改良を行う。
【０００３】
静的解析技術は、所与のプログラムの到達可能な状態の集合の健全な過度近似を計算する。このような過度近似は、適切に選ばれた抽象ドメイン内の不動点であるとして、抽象的解釈を使用して、計算される。抽象的解釈は、抽象ドメインの賢明な選択によって、解析の精度を制御する。
【発明の開示】
【発明が解決しようとする課題】
【０００４】
静的アナライザーは、過度近似によって誤検出を報告する恐れがある。上述のように、過度近似のために失われた精度は、経路依存解析、分離的完了、及びドメイン改良のような技術によって、ある程度回復できる可能性がある。経路依存解析は、孤立しているプログラム経路の異なる集合について推論し、したがって、プログラムのマージ・ポイントにおける結合演算のインパクトを極小化する。しかし、完全に経路に依存する解析は、実際には禁止的な費用を要する。したがって、性質を何時でも証明するのに適当な、ある程度の経路依存性を実現するために、多くの静的解析アルゴリズムは、異なる経路による寄与を選択的に結合あるいは分離する中間的な解を目指す。このような方法は、解析において異なる経路からの寄与を混合するべきか、あるいは、別の論理和としてそれらを保持するべきか、を決定するための発見的学習法に依存している。
【０００５】
抽象的解釈についての最近の研究は、より正確な結果を段階的に得るために、初期の抽象ドメインあるいは反復自身の改良に焦点を合わせている。実際には、本発明では、プログラムの制御流れ図（ＣＦＧ）表現における多くの構文的経路は、意味論的に実行不可能であることを発見した、すなわち、それらはプログラムのいかなる実行によってもトラバースされる可能性はない。このような経路の実行不可能性についての推論は、正しいアプリケーション・プログラム・インタフェイス（ＡＰＩ）使用法、空ポインタ・デリファレンスの欠落、ならびに、変数、メモリ・リーク、等の初期化されていない使用、のような性質をチェックするために、正確な静的解析を行うに当たって、重要な要因である。
【課題を解決するための手段】
【０００６】
経路依存の抽象インタプリターの構築に関する従来の経験は、静的解析に経路依存性を追加する利益が、主として意味論的に実行不可能な経路の識別と除外にあるように思われることを示している。経路に依存しない解析は、解析が複雑な抽象ドメインに対して実行されない限り、このような実行不可能な経路は一般に推論不可能である。さらに、関心のある性質が構文的である場合でも、（たとえば、ＡＰＩ呼出し手順のチェック）通常その解決は、プログラム内の数値的及び記号的データ要素を推論する能力次第であり、これは意味論的により豊かなドメインを必要とする。本発明の実施形態の目標は、経路に依存しない解析を基本的に使用して、プログラムにおける経路依存の推論の利益を得るための新しい方法を提供することである。本発明は、プログラム内の意味論的に実行不可能な経路の集合を特徴付け、列挙するための、抽象的解釈方式を提案する。本発明による方法は、実行不可能な経路を検出するために、経路に依存しない抽象インタプリターを使用して、一連の多くの順方向及び逆方向のランを行う。次に、既に列挙した経路の繰り返しを避けるために、命題ＳＡＴソルバーと理論満足化可能性チェッカーの組み合わせを使用して、列挙技術を使用する。次に、制御流れ図（ＣＦＧ）内の構文的経路の集合を連続して改良するために、本発明では、実行不可能な経路検出を組み合わせる。そうすることによって、他の場合には経路依存解析を必要とするであろう証明を推測するために、基礎をなしている経路に依存しない解析が使用可能である。
【０００７】
本発明による方法は、（ａ）健全性を犠牲にせずに、ループ、状態、手順、等を処理するために、組織的な方法で抽象的解釈を使用する。（ｂ）経路に依存しない実行不可能な経路を検出するための基礎をなしている解析方法を使用する。これは、多くのオーバーヘッドあるいは深度カットオフ（depth cutoffs）を必要とせずに、全プログラム・ベースで本方法の適用を可能にする。本発明による方法は、合理的なオーバーヘッドで、より多くの性質を証明することが可能なアナライザー・ツールに実現された。
【０００８】
実行不可能な経路検出のためのシステム及び方法は、プログラムの性質を証明するためにプログラムの静的解析を行うことを含んでいる。性質が証明されなければ、経路に依存しない抽象的解釈を行うことにより、プログラムの実行不可能な経路が決定される。このような実行不可能な経路についての情報は、経路に依存しないプログラム解析において、経路依存性の効果を実現するために使用される。
【０００９】
実行不可能な経路検出のためのシステムは、プログラムの性質を証明するためにプログラムに対して静的解析を行うように構成された抽象的解釈エンジンを含んでいる。エンジンは、プログラム・ポイントにおける到達可能なプログラム状態に対応するアサーションを決定するために、抽象ドメインを使用する一連の経路に依存しない順方向及び逆方向の伝搬によって、経路に依存しない抽象的解釈を行うように構成されている。満足化可能性ソルバー、及び理論満足化可能性チェッカーは、プログラム内の実行不可能な経路を決定するために、連合が論理的に偽であるアサーションの部分集合を生成するように、組み合わせて使用される。
【００１０】
以上の特徴と他の特徴ならびに利点は、添付図面に関連して読まれるべき例証的実施形態の下記の詳細説明から明白であろう。
【発明を実施するための最良の形態】
【００１１】
本発明の原理は、抽象的解釈を使用して、プログラム内の意味論的に実行不可能な経路を検出する。本明細書において説明することは、実行不可能性を検出する技術であり、この技術は、間隔及び八角形のような一般に使用された抽象ドメインに対して、インスタンス生成される。本発明による方法は、プログラムの具体的な実行では使用される機会のない経路を推測するために、適切な抽象ドメインを使用して、抽象インタプリターの一連の経路に依存しない順方向及び逆方向のランを使用する。
【００１２】
次に本明細書では、解析の結果を反復して改善するために、抽象インタプリターの後続のランで、本発明による方法によって推測した意味論的に実行不可能な経路を除外する構文上の言語改良（ＳＬＲ）技術を提案する。具体的にいうと、基本的な経路に依存しない静的アナライザーにおいて構文上の言語改良を使用することによって、本発明では経路依存解析の効果を段階的に得ることが可能である。Ｃプログラムの抽象インタプリター上で本発明による方法のインパクトを数量化するために、実験結果が得られた。
【００１３】
抽象的解釈を使用して実行不可能な経路部分を検出し列挙するために、本明細書では組織的な方法が提供される。従来の方法は、特別な目的のためのものであり、ループの取り扱いは不完全であり、仮定はプログラムの性質／構造についてなされ、実行不可能性の特定のパターンのみを処理することができる。列挙された実行不可能な経路部分の解は、経路依存解析の効果を得るために、使用される。これは、経路依存解析が、主として実行不可能な経路を除外することにより精度を得ているという洞察にもとづいている。したがって、本発明による方法は、より直接である。
【００１４】
本明細書において説明する実施形態は、完全にハードウェア、完全にソフトウェア、あるいは、ハードウェア及びソフトウェア要素の両方を含むものでもよい。推奨実施形態において、本発明は、ファームウェア、常駐ソフトウェア、マイクロコード等を含むが、それに制限されないソフトウェアで、実現される。
【００１５】
本発明の原理は、経路に依存しない解析を使用する実行不可能な経路の検出と、経路に依存する解析に類似のより良い結果を得るために、検出された経路の使用とを含む。プログラム内で実行不可能な経路を検出するために、経路に依存しない抽象的解釈を使用する異なる技術が提供される。このような経路は、プログラムのいかなる実行によってもトラバースされないことを保証される。実行不可能性検出器の結果を使用して、これらの実行不可能な経路をプログラムから除去するために、本発明では、構文上の言語改良を行う。結果として生ずるプログラムは依然として、制御流れ図（ＣＦＧ）表現を使用して、表現することが可能である。このプログラム上の経路に依存しない解析は、より多くの実行不可能な経路を除外し、したがって、プログラム構造のさらなる改良を可能にする。結局、他の状況では経路依存の推論を要するであろう性質の証明を可能にするために、この改良は十分である。その間中ずっと、この方法は、その基本的静的解析として、経路に依存しない解析を使用する。
【００１６】
実施形態は、コンピュータあるいは任意の命令実行システムによって、あるいは、それに関連して使用する、プログラム・コードを提供するコンピュータで使用可能な、あるいはコンピュータで読み取り可能な媒体からアクセス可能なコンピュータ・プログラム・プロダクトを含むことが可能である。コンピュータで使用可能な、あるいはコンピュータで読み取り可能な媒体は、命令実行システム、装置、あるいはデバイスによって、あるいは、それに関連して使用するためのプログラムを、蓄積し、通信し、伝搬し、あるいは運搬する任意の装置を有してもよい。媒体は、磁気的、光学的、電子的、電磁気的、赤外線、あるいは半導体システム（あるいは装置あるいはデバイス）あるいは伝搬媒体とすることが可能である。媒体は、半導体、あるいはソリッド・ステート・メモリ、磁気テープ、取外し可能なコンピュータ・ディスケット、ランダム・アクセス・メモリ（ＲＡＭ）、リード・オンリー・メモリ（ＲＯＭ）、磁気ハード・ディスク、ならびに、光ディスク、等のような、コンピュータ読み取り可能な媒体を含むことが可能である。
【００１７】
ここで図面を参照すると、類似の番号は同じ、あるいは類似の要素を表す。初めに図１は、静的解析において一般に起きる状態を表す例のプログラムを示す。図１の左はプログラム・コードであり、図１の右はプログラムに対応している対応する制御流れ図（ＣＦＧ）である。最初に変数の符号が評価され、結果はフラグ変数ｆに置かれる。後に、ｆにもとづいた状態が、ｎを間接的に含むアサーションを保護する。多面抽象ドメインを使用する経路に依存しない静的解析は、ノードｎ３における結合を計算することによりｆとｘの間の相関を失うために、性質を証明することが不可能である。他方、本明細書において提案する技術は、経路に依存しない解析を使用して、ノードｎ0からノードｎ4迄の任意の意味論的に実行可能な経路がノードｎ2を通過することが不可能であることの証明を可能にする。構文上の言語改良は、この経路をＣＦＧから除去し、ＣＦＧの残りの経路に新しい経路に依存しない解析を行う。このような解析は、ノードｎ3におけるｘとｆの間の相関を維持し、性質を成功裡に証明する。
【００１８】
図２に、抽象的解釈を使用する実行不可能な経路を決定するためのシステム／方法を実例として示す。解析されるべきプログラム２０２は、実行不可能な経路計数器２０４に入力される。計数器２０４は、実行不可能な経路を決定するために、プログラム２０２を解析し、データベース２０６に実行不可能な経路を出力する。計数器２０４は、抽象的解釈エンジン２１０を有することが望ましい。エンジン２１０は、プログラム２０２の各点において、抽象的解釈あるいは等価な方法を使用して、到達可能な状態の過度近似を識別するために使用される。このエンジン２１０は、各プログラムの位置から開始して、利用者により選択された一定の方向でプログラム２０２を解析して、複数回実行される。この方法は、現在のプログラム・ポイントからプログラムの終わり迄の順方向の抽象的解釈に対して、あるいは、現在の位置から初期のノード迄の逆方向の抽象的解釈に対して、機能を発揮する。結果として、各プログラム・ポイントｉに対応するアサーションＰiを得る。
【００１９】
満足化可能性（ＳＡＴ）２１２ソルバーは、エンジン２１０からの抽象的解釈の結果にもとづいて、実行不可能なプログラム内の経路を列挙するために使用される。ＳＡＴソルバー２１２は、プログラム経路と状態が満足できるか否かを決定するために、プログラム・コードをチェックするために、満足化可能性チェッカー２１４と共に機能を発揮する。
【００２０】
プログラム位置１，２，．．．，ｎにそれぞれ対応するアサーションｐ1，Ｐ2，．．．，Ｐnを仮定して、その連合が論理的に偽であるＰi，．．．，Ｐnのすべての部分集合を生成するために、ＳＡＴソルバー２１２、及び、ＵＮＳＡＴコア生成を有する理論満足化可能性チェッカー２１４の組み合わせを使用する。１つの観察では、このような連合のそれぞれに対応するプログラム・ポイント１．．．．ｎが、実行不可能な経路を生じさせる。このような実行不可能な経路は、データベース２０６に記録される。
【００２１】
計数器２０４は、抽象的解釈を使用して、実行不可能な経路部分を系統的に発見し、列挙する。これは、たとえば、ループの完全な処理を提供し、プログラムの性質／構造についての仮定を行う必要なく実行される。
【００２２】
上述の方式は、実行不可能な経路計数器を構築するために、所与の抽象的解釈エンジン（市販の）を使用して実行することができる。
【００２３】
図３において、経路に依存する解析をシミュレートするために、経路に依存しない解析を使用するシステム／方法は実例を示す表示である。図２の実行不可能な経路のデータベース２０６を使用して、経路依存解析の効果が得られる。これは、実行不可能な経路を除外することにより、経路依存解析が精度を得るとの洞察にもとづいている。したがって、この方法は、より直接的である。
【００２４】
経路依存解析を行うために、（実行不可能な）検出された経路は使用され、ソフトウェア・テスト、述語抽象化、ＡＰＩ使用法解析、等で使用することができる。性質試験（property proofs）を、より多く発見し、プログラム２０２のバグを、より多く間接的に（ＳＡＴ２１２ソルバーの使用により）発見して、より良いプログラム解析を行うために、図３では、以前に得られた実行不可能な経路を使用する。これは構文上の言語改良（ＳＬＲ）と呼ばれ、次のように動作する。ブロック３０２において、現在のプログラム（２０２）を解析する。ブロック３０４において、ブロック３０２における解析が、関心事の性質を証明したら（たとえば、安全性が証明された）、ブロック３０６で終了する。他の場合には、ブロック３０８において、実行不可能な経路を決定するために、現在のプログラムに対して図２で説明した実行不可能な経路列挙を実行し、これらの実行不可能な経路をプログラムのＣＦＧ記述から除外する。これは、結果を改善するために、ＳＬＲを使用することを含んでいる。ブロック３１０において決定されたように、プログラムが変更されていれば、プログラム経路はブロック３０２に戻る。他の場合には、プログラム経路は、ブロック３１２で終了する。
【００２５】
この処理において、ブロック３０２から、３０４、３０８、３１０までを反復し、その都度、ますます多くの意味論的に実行不可能であると判明したプログラム経路を除去する。これは、適切な解析をもたらし、より価値の高い経路依存解析の効果をシミュレートすることを示した。
【００２６】
完全を期すために、プログラム・モデル、抽象的解釈、抽象ドメイン、及びいくつかの一般に使用される数値的ドメインを、次に説明する。本開示を通じて、整数変数の単一手順の（ｗｈｉｌｅ）プログラムを、例として使用する。しかし、本発明による結果は、多くの手順と複雑なデータ型を有するプログラムに拡張される。
【００２７】
プログラムは、〈Ｍ，Ｅ，μ，ｎ0，ψ0〉で示す制御流れ図（ＣＦＧ）により表さる。ここで、Ｎは１組のノードであり、Ｅ⊆Ｎ×Ｎはノード間の１組のエッジであり、ｎ0∈Ｎは初期の位置である。各エッジｅ∈Ｅは、状態あるいはアップデートμ（ｅ）によって、ラベルを付けられる。アサーションψ0は、実行の開始時に保持するプログラム変数の状態を指定する。
【００２８】
プログラムの状態は、プログラム変数のそれぞれに対して整数の付値を有する。Σを、すべてのこのような付値の母集団であるとする。プログラムは、ψ０を満足する状態の初期位置から開始すると仮定する。エッジｅ∈Ｅのセマンティクスは、（具体的な）事後条件
【００２９】
【数１】
2009176282.tif 000003
【００３０】
あるいは、集合ｓ∈Σに対する（具体的な）最も弱い事前条件（逆方向の事後条件）
【００３１】
【数２】
2009176282.tif 000004
【００３２】
により記述できる。ｐｏｓｔ（ｅ，Ｓ）演算子は、状態Ｓの所与の集合からエッジを実行して到達可能な状態の最小の集合をもたらし、一方、ｐｒｅ（ｅ，Ｓ）演算子は
【００３３】
【数３】
2009176282.tif 000005
【００３４】
であるような最小の集合Ｔをもたらす。事前条件は、エッジｅに対する逆遷移関係の事後条件にも対応する。
【００３５】
順方向伝搬
マップ
【００３６】
【数４】
2009176282.tif 000006
【００３７】
は、１組の状態をＣＦＧ内の各ノードと関連付ける。便宜上、集合包含（set inclusion）を、η1⊆η2として、マップにリフトする。マップηは、次式の場合にのみ帰納（事後不動点）マップである。
【００３８】
【数５】
2009176282.tif 000007
【００３９】
到達可能な状態ｒｅａｃｈ（・）の集合も、最小帰納的マップである。任意の帰納マップも、次式のマップ上の順方向伝搬演算子
【００４０】
【数６】
2009176282.tif 000008
【００４１】
の事後不動点である。
【００４２】
【数７】
2009176282.tif 000009
【００４３】
特に、最小帰納的マップも、具体的格子２Σ内の演算子Ｓの最小不動点である。ＣＦＧを仮定すると、性質は対〈ｎ、ψ〉から成り、ここで、ｎ∈Ｎはノードであり、ψは１組の状態を表す１次のアサーションである。性質〈ｎ，ψ〉は、帰納マップηに対して、
【００４４】
【数８】
2009176282.tif 000010
【００４５】
であるかを、検証される。
【００４６】
最小帰納的マップは、タルスキー反復を使用して計算できる。ｎ0をψ0にマップし、ＣＦＧ内の他のすべてのノードを０にマップする初期マップη0から開始して、不動点に到達する迄演算子
【００４７】
【数９】
2009176282.tif 000011
【００４８】
を適用する。残念ながら、プログラムが無限状態であれば、この処理は計算上実行不可能である恐れがある。このようなプログラムに対しては、収束するために必要な反復の数は、無限となる恐れがある。第二に、それぞれの反復において、各ノードｎに対する集合ηi（ｎ）は、無限大である恐れがあり、したがって、操作が困難である。したがって、具体的ドメイン上の反復は、実際には実行可能ではない。
【００４９】
この課題を克服するために、不動点の過度近似を計算するために、抽象的解釈が使用される。抽象的解釈の間、状態の集合は、抽象ドメイン内の要素により表される。抽象ドメインは、格子（Ｌ，⊆，∪，∩）、抽象化ドメイン
【００５０】
【数１０】
2009176282.tif 000012
【００５１】
と、具体化マップ
【００５２】
【数１１】
2009176282.tif 000013
【００５３】
から成っている。各抽象オブジェクトα∈Ｌは、１組の状態γ（ａ）⊆Σと組み合わされている。マップα及びγは共に、具体的格子２Σと抽象格子Ｌの間のガロア接続を提供する。和集合（∪）及び交点（∩）に対する抽象対応物は、それぞれ、格子結合（∪）及び格子交点（∩）演算子である。最後に、具体的な事後条件と事前条件は、抽象格子Ｌ内の抽象対応物
【００５４】
【数１２】
2009176282.tif 000014
【００５５】
と
【００５６】
【数１３】
2009176282.tif 000015
【００５７】
を有する。抽象ドメイン・マップ
【００５８】
【数１４】
2009176282.tif 000016
【００５９】
は、各ノードｎ∈Ｎを抽象オブジェクト
【００６０】
【数１５】
2009176282.tif 000017
【００６１】
に関連付ける。格子順序付け⊆は、次式のように、Λに当然に持ち上げられることができる。
【００６２】
【数１６】
2009176282.tif 000018
【００６３】
の場合にのみ
【００６４】
【数１７】
2009176282.tif 000019
【００６５】
具体的ドメイン内の順方向伝搬演算子
【００６６】
【数１８】
2009176282.tif 000020
【００６７】
に対応して、格子Ｌ内の類似した抽象順方向伝搬演算子
【００６８】
【数１９】
2009176282.tif 000021
【００６９】
を、次式のように、定義することが可能である。
【００７０】
【数２０】
2009176282.tif 000022
【００７１】
所与のプログラムに対して、抽象的解釈は、初期のマップ
【００７２】
【数２１】
2009176282.tif 000023
【００７３】
で、開始する。ここで、すべてのｍ≠ｎ0に対して、
【００７４】
【数２２】
2009176282.tif 000024
【００７５】
であり、
【００７６】
【数２３】
2009176282.tif 000025
【００７７】
である。
【００７８】
【数２４】
2009176282.tif 000026
【００７９】
を適用することにより、各連続したマップが得られる。したがって、
【００８０】
【数２５】
2009176282.tif 000027
【００８１】
となる。
【００８２】
【数２６】
2009176282.tif 000028
【００８３】
であれば、処理は、Ｌ内での不動点
【００８４】
【数２７】
2009176282.tif 000029
【００８５】
に収束する。さらに、その具体化
【００８６】
【数２８】
2009176282.tif 000030
【００８７】
は、具体的格子上の帰納（事後不動点）である。実際には、抽象格子内の反復の収束を行うために、拡張／狭窄のような発見的学習法を使用できる。
【００８８】
逆方向伝搬
プログラム内の所与の性質〈ｎ，ψ〉を検証することの代案は、
【００８９】
【数２９】
2009176282.tif 000031
【００９０】
演算子を使用する逆方向伝搬である。本明細書では、逆方向伝搬演算子φ’＝Ｂ（φ）を使用して、最小不動点を計算する。
【００９１】
【数３０】
2009176282.tif 000032
【００９２】
すべてのｍ≠ｎに対して、
【００９３】
【数３１】
2009176282.tif 000033
【００９４】
であり、φ0（ｍ）＝０であるような、初期マップφ0を使用して、開始する。Ｂ（φ）⊆φであれば、マップφは、演算子Ｂの事後不動点である。φは、Ｂの事後不動点であるとする。したがって、任意の位置ｌに対して、ｌから開始して性質〈ｎ，ψ〉に違反する実行が存在すれば、このような実行はφ（ｌ）を満足させる状態から開始しなければならないことになる。直接の結果として、
【００９５】
【数３２】
2009176282.tif 000034
【００９６】
であれば、性質は設定できる。
【００９７】
順方向伝搬に類似して、抽象ドメイン内で解釈した事前条件マップ
【００９８】
【数３３】
2009176282.tif 000035
【００９９】
を使用して、抽象逆方向伝搬演算子ＢＬを定義することによって、抽象ドメイン（Ｌ，⊆，∪，∩）内の逆方向の（事後）不動点マップφ#を計算することが可能である。逆方向の不動点は、さらに、性質〈ｎ，ψ〉を検証するために使用可能な帰納マップを帰納する。
【０１００】
実行不可能な経路検出
ここで、経路に依存しない抽象的解釈を使用して、プログラム内の実行不可能な経路を記述する。（無限に多数が存在し得る）個別の経路に焦点を合わせるのではなく、本発明の結果では、実行不可能な経路の集合を簡潔に記述する。順方向射影演算子
【０１０１】
【数３４】
2009176282.tif 000036
【０１０２】
と逆方向射影演算子ＢＬを得る所与の抽象ドメイン（Ｌ，⊆，∪，∩）（あるいは多数の抽象ドメインの組み合わせでも）を仮定する。変化する状態を有する初期のマップη0（φ0）を仮定すると、これらの演算子は、格子Ｌ内の（事後）不動点をもたらし、順に、具体化マップγを使用する合成によって、具体的ドメイン内の（事後）不動点をもたらす。
【０１０３】
組の状態
【０１０４】
【数３５】
2009176282.tif 000037
【０１０５】
に加えて、ノードｎ∈Ｎを考える。ここで、対〈ｎ，ψ〉のノードｎ’∈Ｎへの順方向及び逆方向射影を定義する。対〈ｎ，ψ〉を仮定して、次の初期マップから開始して、順方向の不動点ηＦ及び逆方向の不動点ηＢを計算する。
【０１０６】
【数３６】
2009176282.tif 000038
【０１０７】
不動点ηＦ及びηＢは、ｎからｎ’へ順方向及び逆方向に、状態集合
【０１０８】
【数３７】
2009176282.tif 000039
【０１０９】
の射影を可能にする。
【０１１０】
定義１（状態集合射影）
【０１１１】
【数３８】
2009176282.tif 000040
【０１１２】
で示されるノードｎ’への対〈ｎ，ψ〉の順方向射影は、集合
【０１１３】
【数３９】
2009176282.tif 000041
【０１１４】
であり、ここで、ηＦは、初期マップ
【０１１５】
【数４０】
2009176282.tif 000042
【０１１６】
から始まる
【０１１７】
【数４１】
2009176282.tif 000043
【０１１８】
の（事後）不動点である。
【０１１９】
同様に、
【０１２０】
【数４２】
2009176282.tif 000044
【０１２１】
で示される逆方向にｎ’への対〈ｎ，ψ〉の逆方向射影は、集合
【０１２２】
【数４３】
2009176282.tif 000045
【０１２３】
であり、ここで、ηＢは、初期マップ
【０１２４】
【数４４】
2009176282.tif 000046
【０１２５】
から始まるＢＬの（事後）不動点である。ノードｎの自身への射影は、アサーション真であることに注目されたい。次の補助定理は、抽象的解釈の適切さの結果として生じる。
【０１２６】
補助定理１
【０１２７】
【数４５】
2009176282.tif 000047
【０１２８】
及び
【０１２９】
【数４６】
2009176282.tif 000048
【０１３０】
は、それぞれ、ｎ’への対
【０１３１】
【数４７】
2009176282.tif 000049
【０１３２】
の順方向及び逆方向の射影を示すとする。次のことが、状態集合射影に対して適用される。
【０１３３】
１）ノードｎにおいて状態
【０１３４】
【数４８】
2009176282.tif 000050
【０１３５】
から開始する実行が、状態ｓ’であるノードｎ’に到達すれば、
【０１３６】
【数４９】
2009176282.tif 000051
【０１３７】
である。
【０１３８】
２）状態ｓ’であるノードｎ’から開始する実行が、状態
【０１３９】
【数５０】
2009176282.tif 000052
【０１４０】
であるノードｎに到達すれば、
【０１４１】
【数５１】
2009176282.tif 000053
【０１４２】
である。
【０１４３】
実行不可能性定理
順方向及び逆方向の伝搬を使用して計算された状態集合射影は、ＣＦＧ内の意味論的に実行不可能な経路を検出するために使用できる。ｎ1，．．．，ｎkはＣＦＧ内のノードであり、ｎ0は初期ノードであり、また、ｎk+1は関心のある何らかの目標ノードであるとする。ノードｎ1，．．．，ｎkのそれぞれを、できる限り２回以上、任意の順序で通過する間に、ｎ０から開始して実行がｎk+1に到達可能であるかを発見することが望ましい。Π（ｎ0，．．．，ｎk+1）は、ＣＦＧ内のすべてのそのような構文上有効な経路の集合であるとする。
【０１４４】
【数５２】
2009176282.tif 000054
【０１４５】
は、〈ｎi，ｔｒｕｅ〉から最後のノードｎｋ＋１への順方向の状態集合射影を示すとする。同様に、
【０１４６】
【数５３】
2009176282.tif 000055
【０１４７】
は、〈ｎi，ｔｒｕｅ〉からノードｎ０への逆方向の状態集合射影を示すとする。
【０１４８】
定理１（実行不可能型定理）
Π（ｎ0，．．．，ｎk+1）内の経路は、次式のいずれかであれば、すべて意味論的に実行不可能である。
【０１４９】
１．ψ0∧ψ1∧．．．．．∧ψk∧ψk+1≡ｆａ１ｓｅ、あるいは、
２．Ψ0∧Ψ1∧．．．．．∧Ψk∧Ψk+1≡ｆａ１ｓｅ
状態集合射影を使用して、他の実行不可能型定理を定式化することも、可能である。ηFは、〈ｎ0，ψ0〉から開始して計算された順方向の不動点マップであるとする。
【０１５０】
【数５４】
2009176282.tif 000056
【０１５１】
は、ノードｎiからノードｎ0への集合
【０１５２】
【数５５】
2009176282.tif 000057
【０１５３】
の状態集合射影であるとする。
【０１５４】
補助定理２
ψ1∧．．．．．∧ψk∧ψk+1≡ｆａ１ｓｅであれば、ｎ1，．．．，ｎkのすべてを通過するノードｎ0からノードｎk+1への意味論的に有効な経路は存在しない。順方向及び逆方向の不動点マップを使用して、一対のノードに対して、類似の結果を述べることができる。〈ｎ，ψ〉は関心のある性質であり、ηF及びηBは〈ｎ0，ψ0〉から開始して計算された順方向の（事後）不動点マップであり、ηBは〈ｎ，−ψ〉から開始して計算された逆方向の（事後）不動点マップであるとする。
【０１５５】
補助定理３
ηF（ｎ’）∧ηB（ｎ’）≡ｆａｌｓｅであれば、〈ｎ，ψ〉に違反するいかなる誤り中断（error truce）も、ノードｎ’を訪れることはできない。図１に示す実例のプログラムを考える。ｎ0、ｎ2、及びｎ4を同時に訪れる任意の経路の実行不可能性を証明することが望ましい 。そうするために、ｎ2及びｎ4から開始してｎ0への状態の逆方向射影を行う。間隔抽象ドメインを使用して、射影が実行されると仮定する。〈ｎ2，ｔｒｕｅ〉の逆方向射影は、ψ2：ｘ≦０をもたらす。同様に、〈ｎ4，ｔｒｕｅ〉の逆方向射影は、ψ4：ｘ＞０をもたらす。ψ2とψ4は相互に矛盾しているから、ＣＦＧの実行が、ノードｎ0、ｎ2、及びｎ4を訪れることは不可能である。同様に、〈ｎ0，ｔｒｕｅ〉のｎ4への順方向射影は、アサーションψ0：ｆ＞０をもたらす。〈ｎ2，ｔｒｕｅ〉のｎ4への順方向射影は、アサーションψ2：ｆａｌｓｅをもたらす。したがって、ｎ0、ｎ2、及びｎ4を同時に訪れることは、意味論的に有効な経路に対して、不可能である。
【０１５６】
実行不可能な経路の列挙
状態集合射影を使用して、意味論的に実行不可能な経路を記述した。これらの結果は、ノードｎ0，．．．，ｎkの所与の集合に対して、Π（ｎ0，．．．，ｎk+1）が意味論的に実行不可能であるか否かを検出するために、適用することができる。ここで、このような集合を列挙する問題を考える。
【０１５７】
Ｎ＝｛ｎ0，ｎ1，．．．，ｎm｝は、ＣＦＧ内のすべてのノードの集合を示すとする。既に説明した実行不可能性の結果（たとえば、定理１及び補助定理２）から、各定理は、それぞれノードｎ0，．．．，ｎmに対応する状態集合射影Ψ0，．．．，Ψmを計算することに注目する。さらに、部分集合｛ｎh，．．．，ｎk｝を横断する経路が意味論的に実行不可能であるか否かを試験するために、連合Ψh∧．．．．．∧Ψkが満足し得ないか否かを調べる。
【０１５８】
したがって、すべてのこのような部分集合を列挙するために、
【０１５９】
【数５６】
2009176282.tif 000058
【０１６０】
であるようなすべてのインデックス集合Ｉ⊂｛１，．．．，ｍ｝を単に列挙する。そのような集合Ｉのそれぞれに対して、Ｎの対応する部分集合は、意味論的に無効な経路を記述する。
【０１６１】
定義２（実行不可能で、飽和したインデックス集合）      アサーションψ1，．．．．．，ψmを仮定すると、インデックス集合ｌ⊂｛１，．．．，ｍ｝は、
【０１６２】
【数５７】
2009176282.tif 000059
【０１６３】
の場合にのみ、実行不可能であると言われる。同様に、実行不可能なインデックス集合ｌは、適切な部分集合自身が実行不可能ではない場合にのみ、飽和したと言われる。各実行不可能な集合は、アサーションψ1∧．．．．．∧ψmの満足し得ないコアであることに注目されたい。各飽和した実行不可能な集合は、（集合包含に対して）最小の満足し得ないコアである。アサーションψ1．．．．．ψmを仮定して、本発明では、すべての飽和した実行不可能なインデックス集合を列挙しようと努める。この課題を解くために、本発明では、列挙を支援するために、ＳＡＴソルバーを使用する一般的な方法を提供する。次に、非満足化可能性コアの空間の中で直接探索可能な別の列挙技術を提供するために、一般的な列挙技術を、間隔、八角形、及び多面体のような数値的抽象ドメインに特化する。
【０１６４】
一般的な列挙技術
インデックス集合Ｉ⊆｛１，．．．，ｍ｝に対応する結合数式（conjunctive formula）
【０１６５】
【数５８】
2009176282.tif 000060
【０１６６】
の満足化可能性をチェックするオラクルＯを想定する。各要素ｉ∈Ｉを除外し、Ψ１が除外されたときにΨ1が満足し得るに到るか否かを調べることによって、最小コア・インデックス集合Ｊ⊆Ｉを抽出することが可能である。あるいは、０自身が最小コア・インデックス集合Ｊ⊆Ｉの提供が可能であってもよい。
【０１６７】
Ｏを仮定して、本発明による手順は、可能性に対してチェックされていない部分集合
【０１６８】
【数５９】
2009176282.tif 000061
【０１６９】
のファミリーを維持する。初めに、すべての可能な部分集合から成る集合
【０１７０】
【数６０】
2009176282.tif 000062
【０１７１】
を設定する。各反復は、２つの段階を有する。
【０１７２】
１）試験されていない部分集合
【０１７３】
【数６１】
2009176282.tif 000063
【０１７４】
を選ぶ。
【０１７５】
２）
【０１７６】
【数６２】
2009176282.tif 000064
【０１７７】
の満足化可能性をチェックする。
【０１７８】
ΨJが満足し得るならば、集合
【０１７９】
【数６３】
2009176282.tif 000065
【０１８０】
からＪを除外する。ΨJが満足し得ないならば、Ｉ⊆Ｊを最小のコアであるとする。Ｊのすべてのスーパーセットを
【０１８１】
【数６４】
2009176282.tif 000066
【０１８２】
から除外する。
【０１８３】
【数６５】
2009176282.tif 000067
【０１８４】
から開始して、
【０１８５】
【数６６】
2009176282.tif 000068
【０１８６】
に到るまで、既に概要を説明した段階（１）及び（２）を実行する。
【０１８７】
ＳＡＴを使用する記号列挙
実際には、集合
【０１８８】
【数６７】
2009176282.tif 000069
【０１８９】
は、明示的に維持するには大き過ぎる恐れがある。したがって、ＳＡＴ数式で簡潔に符号化することが便利である。本発明では、ブーリアン・セレクタ変数ｙ1，．．．，ｙmを導入する。ここで、ｙiは各命題（conjunct）にアサーションψiの存在を示す。集合
【０１９０】
【数６８】
2009176282.tif 000070
【０１９１】
は、セレクター上にブーリアン数式
【０１９２】
【数６９】
2009176282.tif 000071
【０１９３】
によって簡潔に表される。初期の数式
【０１９４】
【数７０】
2009176282.tif 000072
【０１９５】
は真に設定される。各段階において、新しいクローズ
【０１９６】
【数７１】
2009176282.tif 000073
【０１９７】
を付け加えることにより、集合Ｊのすべてのスーパーセットを除外してもよい。
【０１９８】
最適化として、ＣＦＧからの一部の情報を符号化することによって、構文的に実行不可能な経路を考慮しない。ｎ0から開始してｎiとｎjの両方を訪れる構文的経路が存在しない場合には、ノードｎi及びｎjは対立する。Ｃ⊆Ｎ×Ｎは、すべての対立するノード対の集合を示すとする。各対立対（ｎi，ｎj）∈Ｃにクローズ
【０１９９】
【数７２】
2009176282.tif 000074
【０２００】
を付け加えることにより、対立するノードあるいはそれらのスーパーセットを列挙処理から除外する。これは、対立する対を有する集合を列挙から除外する。
【０２０１】
図４は、ＳＡＴソルバー及び満足し得ないコアの除去を使用して、すべての実行不可能なインデックスを列挙するための、説明的な手順を示す。一般的な経路列挙技術は、意味論的に実行不可能な経路に対応するすべての実行不可能なインデックス集合を列挙する。他方、大部分の実行不可能な集合は、少数のノードを含むと考えられる。上述の技術を、サイズが有界である集合を選択ように、適合することは可能である。多くても２つのノードを含む実行不可能な経路に対して、順方向の不動点マップをｎ0から計算し、逆方向の不動点マップを目標ノードｎから計算することに、単純にもとづく、より強力な方式を得るために、補助定理３を使用することが可能である。
【０２０２】
ＳＡＴを使用するグラフ・ベースの列挙
図に示すように、図４の手順は、ＣＦＧの構造を考慮していない。構文的に実行不可能な経路を除外するために、構文的な対立クローズを加えることが可能である。しかし、図４の手順を修正することにより得られたグラフ・ベースの列挙方式を使用することにより、より多くの部分集合を考慮から除外することが可能である。
【０２０３】
例
そのノード及びエッジにおける実際の動作を無視して、図１のＣＦＧスケルトンを考える。ノードｎ0とｎ5の間のすべての経路が実行不可能である、すなわち、｛０，５｝は、飽和した実行不可能なインデックス集合であると、判明したと仮定する。明らかに、ＣＦＧの構造のために、ノードｎ5へのすべての経路はノードｎ3を通過しなければならないので、インデックス集合｛０，３｝の満足化可能性をチェックする必要はない。しかし、この情報は、ＳＡＴソルバーには利用でず、ＳＡＴソルバーは候補インデックス集合｛０，３｝を生成し、対応する各命題は理論ソルバーによってチェックされる。
【０２０４】
列挙の一部としてＣＦＧ構造を直接符号化するＳＡＴを使用するグラフ・ベースの列挙を使用することができる。これは、ＣＦＧ内の連続した構文的経路に対応するインデックス集合のみを列挙する。ｐ1，ｐ2，．．．，ｐmは、ノードｎi（ｍ≧１）の先行点のインデックスを示し、ｓ1，ｓ2，．．．，ｓrは、ノードｎi（ｒ≧１）の後続点のインデックスを示すと仮定する。ＣＦＧ内の各ノードｎiに対応して、次の制約条件を追加することにより、グラフ構造を符号化する。
順方向：ｍ＞０であれば、
【０２０５】
【数７３】
2009176282.tif 000075
【０２０６】
を追加。
逆方向：ｎ＞０であれば、
【０２０７】
【数７４】
2009176282.tif 000076
【０２０８】
実際には、ｎiが経路（インデックス集合）上に含まれている場合には、その先行（及び、後続）ノードの少なくとも１つも含まれているように、インデックス集合Ｉを強制する。前と同じように、ノードのすべての対にも対立集合（Ｃ）を追加する。これらの初期の制約条件の全体のサイズは、ＣＦＧのサイズ（ノードの数、エッジの数）に線形である。しかし、ＳＡＴベースの列挙は当然ながらすべての（おそらく、指数関数的な数の）構文的経路を考慮する。グラフ・ベースの列挙手順は図４と同様である。図４において、行４は、さらに
【０２０９】
【数７５】
2009176282.tif 000077
【０２１０】
にグラフ・ベースの制約条件を追加する。
【０２１１】
例
図１からＣＦＧスケルトンを再度考えると、インデックス集合｛０，５｝が、ある実行不可能なインデックス集合の満足し得ないコアに存在することが判明すれば、追加のクローズ
【０２１２】
【数７６】
2009176282.tif 000078
【０２１３】
（行１２）は、インデックス集合｛０，３｝のいかなる将来の考慮すべき事項でも防止する。これは、ノードｎ3がインデックス集合に加えられるときに、すべての場合にノードｎ5の追加を過渡的に伴うからである。（後続点ｎ4を介して、あるいは直接の後続点として）しかし、これはブロッキング・クローズによるＳＡＴソルバー内の対立を導き、その結果、インデックス集合｛０，３｝の列挙を妨げる。
【０２１４】
ＭＡＸ−ＳＡＴ技術の利用
原則として、命題のより緊密な統合と理論部分は、既に説明した対立対、及び構文的なグラフベースの制約条件から生じ、ｙ1，．．．，ｙmにわたる、他の命題クローズにしたがって、ＳＭＴ（満足化可能性モジュロ理論）数式の最小の満足し得ない（ＭＵＳ）コアを列挙することにより、得られる。
【０２１５】
【数７７】
2009176282.tif 000079
【０２１６】
ＣＮＦ数式ｆを仮定すると、ＭＡＸ−ＳＡＴ問題は、Ｃに対するいかなる厳密な拡張も満足し得ないように、ｆ内のクローズＣの最大の部分集合を求める。これは、普通のＭＡＸ−ＳＡＴ問題の、（基数に関して）クローズの最大数を満足させる解を求める変形であり、ＮＰハード（NP-hard）に留まる。この問題は、最小の満足し得ないコアを見出す問題と双対である。この二重性は、すべての最小の満足し得ないコアを生成するために、ＭＡＸ−ＳＡＴを解くための手順を使用するために利用できる。満足化可能性をチェックすることは、実際には、非満足化可能性を証明するよりも、容易であると思われるので、これは、より速い方法を導くことが可能である。
【０２１７】
ブーリアン数式のすべての最小の満足し得ないコアを生成するための、公知の２相アルゴリズムが使用可能である。第一の段階は、変化する目標最適化ループで、増分のＳＡＴ手順を使用することによって、すべての最大の解を生成する。第二の段階は、これらの最大の解の（補集合の）集合から、すべての最小の満足し得ないコアを生成することを含んでいる。このような手順は、手順の第一の段階の間にＳＭＴソルバーを置換することにより、本発明の環境で直接使用できる。
【０２１８】
満足し得ないコアを直接列挙
あるドメインでは、連合ψ1∧ψ2∧．．．．．∧ψmのすべての満足し得ないコアを直接列挙することが、可能なこともある。このような列挙が可能であれば、満足し得ないコアのそれぞれは、実行不可能なインデックス集合Ｉ＝｛ｉ｜Ａψ1からの各命題はｕｎｓａｔコアに存在する｝を直接もたらす。この列挙法の利点は、対応する連合が理論的に満足し得る可能性がある考慮中のインデックス集合を、避けることである。第二に、ψ1，．．．．．，ψmを生じる基本的な抽象ドメインの性質は、効率的な列挙のために利用できる。
【０２１９】
ここで、間隔ドメインの中にあるような列挙を考える。間隔ドメインは、形式ｘi∈［ｌiｉ，ｕi］の連合を含んでいる。ψ1，．．．．．，ψmは、間隔解析を使用して実行した状態射影の結果であるとする。結果として、各ψ1は、間隔格子からの抽象要素の具体化である。各ψ1は、満足し得ると仮定する。ψiはアサーション∧ｊｘｊ∈［ｌij，ｕij］であるとする。ここで、それぞれ、ｌijｊ≦ｕijである。次の補助定理は、間隔ドメイン内の関係情報の欠如は、各満足し得ないコアのサイズが最大２に制限されることを示す。
【０２２０】
補助定理４
∧iψi内の任意の満足し得ないコアは、｜ｌij，≦ｕij｜∩｜ｌkj，≦ｕkj｜＝０であるように、正確に２つの各命題：ψi内のｌij≦ｘj≦ｕij、及びｌkj≦ｘj≦ｕkjを含んでいる。結果として、間隔ドメインに対して、ドメイン特有の推論を使用して、実行不可能な経路を列挙することはより効率的である。満足し得ないコアの列挙も、他のドメインで可能である。たとえば、八角形ドメイン内ですべての負のサイクルを発見するか、あるいは、多面体ドメイン内で二重の多面体の頂点を列挙することによって、それを実現することが可能である。
【０２２１】
経路依存解析
実行不可能な経路についての情報は、経路に依存しない解析の正確度を改善するために使用できる。
【０２２２】
例
プログラム（図５の左）及び、その対応するＣＦＧ（図５の右）を図５に示す。プログラムの行９におけるアサーションは、決して違反しない。しかし、表１に射影によって示すように、間隔ドメインを使用する順方向伝搬と逆方向伝搬のいずれも、事実を証明することができない。
【０２２３】
表１：図５のプログラムに対する間隔ドメインに関する順方向及び、逆方向のプロジェクト。
【０２２４】
【表１】
2009176282.tif 000080
【０２２５】
構文上の言語改良
Π〈Ｎ，Ｅ，μ，ｎ０，ψ０〉は、確立されるべき性質〈ｎ，ｆａｌｓｅ〉を有するＣＦＧであるとする。Πは、オートマトン〈ｎ，Ｅ〉として処理することが可能であり、ここで、各ノードｎｉはアルファベット記号を受け取る。ＣＦＧにより表される結果として生ずるオートマトンは、ノードｎ０から開始して、ＣＦＧを通過するすべての構文上有効な経路を受け取る。Ｌｎは、決定論的な有限オートマトンであるとして表されたＣＦＧΠにより受け取られたすべてのノード数列の言語を示すとする。
【０２２６】
前述の章の結果は、ノードｎ０からノードｎへの意味論的に有効な経路が、集合Ｉのすべてのノードを通過しないように、集合Ｉ：｛ｎ1，．．．，ｎk｝⊆Ｎの推測を可能にする。改良手順は、次の段階を実行する。
【０２２７】
１．Π（Ｉ∪｛ｎ0，ｎ｝）＝０であるように、実行不可能なノード集合Ｉ⊆Ｎを列挙する。
【０２２８】
２．各集合Ｉに対して、ＣＦＧの構文上の言語からのすべての経路Π（Ｉ∪｛ｎ0，ｎ｝）を除去する。
【０２２９】
【数７８】
2009176282.tif 000081
【０２３０】
集合Ｌｎ及びＬＩは正則であるから、Ｌn’も正則である。他方、ＣＦＧ内に関数呼出しが存在する状態では、言語Ｌnは文脈自由である。それにもかかわらず、Ｌnが文脈自由であっても、ここで説明した改良手順は、保持を続ける。Π’は、Ｌn’を認識するオートマトンであるとする。
【０２３１】
まず第一に、Ｌn’⊂Ｌnである。第二に、エッジｅ：ｌ→ｍ∈Π’を考える。ｎi、ｎjを、それぞれ、ノードｌ及びｍにラベルを付すアルファベットであるとする。したがって、ｅ’：ｎi→ｎjは、Π内のエッジである。オートマトンΠ’は、次のようにＣＦＧに変換される。
【０２３２】
１．アルファベットｎiによりラベルを付された各ノードｎ’∈Π’に対して、ｎi内の同じ割当をｎ’と関連付ける。
【０２３３】
２．各エッジｌ→ｍ∈Π’に対して、対応するエッジｎi→ｎj∈Πと同じ状態を関連付ける。
【０２３４】
上述の段階１及び２の結果として、ＣＦＧΠの改良Π’を得る。ＣＦＧΠの改良Π’も、同様にＣＦＧである。さらに、Π’内のすべての構文上有効な経路は、同様にΠ内で構文上有効である。したがって、Π’は、構文上有効な経路のより小さい集合を可能にする。結果として、Π’の抽象的解釈は、ＣＦＧ内のノードに対して、より正確な不動点をもたらす可能性がある。
【０２３５】
本発明による方式は、分割ヒューリスティックとして、既に検出された実行不可能なＣＦＧ経路を使用する。これは、本発明による方法の独特のものである。
【０２３６】
例
図３の例に戻って、ノードＩ０：｛ｎ1，ｎ4]、及びＩ１：｛ｎ2，ｎ4｝を横断するｎ0→ｎ5からの経路は、意味論的に実行不可能であることを発見した。したがって、構文上の言語改良（ＳＬＲ）を使用して、このような経路をＣＦＧから除外することが可能である。結果として生ずるＣＦＧΠ’は、ノードｎ4を除外したオリジナルのＣＦＧである。ＣＦＧΠ’上の経路に依存しない抽象インタプリターは、性質の証明に十分である。したがって、経路依存性の効果を得るために、構文上の言語から実行不可能な経路を除外した後で、経路に依存しないアナライザーを使用することによって、検出された実行不可能な経路についての情報を使用することが可能である。
【０２３７】
応用
実際には、ノードのすべての実行不可能な集合の列挙には、多額の費用を要する。したがって、本発明による実行不可能な経路検出の基本原理として補助定理３を使用して、各段階において最大でも１つの中間ノードを除外する言語改良方式の単純なインスタンス生成を考える、すなわち、実行不可能な集合内の中間ノードの集合Ｉのすべては、最大でもサイズが１である。
【０２３８】
経路に依存しない解析を改善するために実行不可能な経路検出を使用する、結果としての構文上の言語改良方式を、例として図６に示す。各段階は、初期ノードからの順方向の不動点と、プロパティ・ノードから計算した逆方向の不動点を含んでいる。第一に、ノードの実行不可能な対が補助定理３を使用して決定され、このような対を含んでいる経路がＣＦＧから除かれる。改良されたＣＦＧに対して順方向の解析を使用して、性質を証明するために、後続の反復が試みられ、性質が証明されれば終了する。実行不可能な性質を検出し、順方向の不動点を計算する反復処理は、性質が検証される迄、繰り返される。あるいは、続く反復で新しいノードが実行不可能であるとして検出されない迄、繰り返される。
【０２３９】
例
プロパティ検証（Verify Property）は、図５に示す例において、アサーションを証明することに注目されたい。再び図５を参照すると、第一の反復の間に、プロパティ検証内の行［８］における状態は、エッジｎ０→ｎ２に対して保持する。したがって、ノードｎ2は、次の順方向の不動点計算の前に、除外される。したがって、間隔解析は、エッジｎ3→ｎ4が実行不可能であると決定することが可能であり、したがって、性質〈ｎ5，ｘ≧０〉が検証される。
【０２４０】
実行不可能な経路検出及び構文上の言語改良によるシステム及び方法経路依存解析の推奨実施形態を説明したが、（これは、例であり、制限的なものではないと意図している、）上記の教示によって当業者には修正及び変形が可能であることが指摘される。したがって、添付した特許請求の範囲により大要を説明するように、本発明の範囲と技術思想の内で、開示されている特定の実施形態において変更が可能であることが、理解されるべきである。特許法により必要とされる詳細と独自性と共に、本発明の態様を以上のように説明したが、特許請求の範囲ならびに特許証による保護を望むものを、添付した特許請求の範囲に詳述する。
【０２４１】
本出願は、２００８年１月２４日に出願され、参考文献として本明細書に包含される、米国仮特許出願番号第６１／０２３，１６１による優先権を主張する。
【図面の簡単な説明】
【０２４２】
【図１】例証的実施形態によって原理を示すための、プログラム・コードと制御流れ略図を示す略図である。
【図２】本発明の原理によるプログラムにおいて、実行不可能な経路を決定するための、システム／方法を示すブロック／フロー・ダイヤグラムである。
【図３】本発明の原理によって図２で決定された実行不可能な経路を使用して、特定の性質を保持し検証するか否かを決定するための、システム／方法を示すブロック／フロー・ダイヤグラムである。
【図４】例証的な実施形態による実行不可能なインデックス集合を列挙するための、ＳＡＴベースの列挙法モジュロ理論に対するプログラム・コードを示す略図である。
【図５】例証的な実施形態による原理を示すための、実例のプログラム及び制御流れ略図を示す略図である。
【図６】例証的な実施形態による経路に依存しない解析を改善するために、実行不可能な経路検出を使用するための、プログラムを示す略図である。
【符号の説明】
【０２４３】
２０２    プログラム
２０４    経路計数器
２０６    データベース
２１０    抽象的解釈エンジン
２１２    ＳＡＴソルバー
２１４    満足化可能性チェッカー
【図１】
2009176282.tif 000082
【図２】
2009176282.tif 000083
【図３】
2009176282.tif 000084
【図４】
2009176282.tif 000085
【図５】
2009176282.tif 000086
【図６】
2009176282.tif 000087