"ソフトウェアを検証する方法であって、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定するステップと、前記初期化の経路の状態は、検証されるべきソフトウェアの開始の状態に到達するためのプログラムのプレディケートのシーケンスを含み、前記受信されたソフトウェアの検証のジョブは、検証されるべきソフトウェアの一部の指示を含み、計算ノードの終了の経路の状態を決定するステップと、前記終了の経路の状態は、前記計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達される最後の状態の指示を含み、前記計算ノードは、前記受信されたソフトウェアの検証のジョブを実行するために割り当てられ、前記初期化の経路の状態と前記終了の経路の状態とに基づいて計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップと、を含むことを特徴とする方法。前記ソフトウェアを検証することは、コードに記号的実行を施すことを含む、請求項1記載の方法。引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップを更に含み、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含む、を含む請求項1記載の方法。引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含み、再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記再生手法は、前記初期化の経路の状態のプレディケートステップを再生することを含み、前記計算されたコストのうちの低い方のコストをもつ初期化の手法を選択するステップと、を更に含む請求項1記載の方法。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、平均の前方向の計算コストを使用することを含み、前記平均の前方向の計算コストは、前記ソフトウェアの検証の間に次のプレディケートに検証の経路に沿って前方向に計算する平均のコストを含む、請求項4記載の方法。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、平均の引き返しの計算コストを使用することを含み、前記平均の引き返しの計算コストは、前記ソフトウェアの検証の間に前のプレディケートに検証の経路に沿って引き返す平均のコストを含む、請求項4記載の方法。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、所与の手法により前記受信されたソフトウェアの検証のジョブの実行を初期化するために必要とされる前方向のステップと引き返しのステップとを使用することを含む、請求項4記載の方法。コンピュータに、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定するステップと、前記初期化の経路の状態は、検証されるべきソフトウェアの開始の状態に到達するためのプログラムのプレディケートのシーケンスを含み、前記受信されたソフトウェアの検証のジョブは、検証されるべきソフトウェアの一部の指示を含み、計算ノードの終了の経路の状態を決定するステップと、前記終了の経路の状態は、前記計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達される最後の状態の指示を含み、前記計算ノードは、前記受信されたソフトウェアの検証のジョブを実行するために割り当てられ、前記初期化の経路の状態と前記終了の経路の状態とに基づいて計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップと、を含むソフトウェアを検証する方法を実行させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。前記ソフトウェアを検証することは、コードに記号的実行を施すことを含む、請求項8記載のコンピュータ読み取り可能な記録媒体。前記方法は、引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップを更に含み、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含む、を含む請求項8記載のコンピュータ読み取り可能な記録媒体。前記方法は、引き返し及び再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含み、再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記再生手法は、前記初期化の経路の状態のプレディケートステップを再生することを含み、前記計算されたコストのうちの低い方のコストをもつ初期化の手法を選択するステップと、を更に含む請求項8記載のコンピュータ読み取り可能な記録媒体。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、平均の前方向の計算コストを使用することを含み、前記平均の前方向の計算コストは、前記ソフトウェアの検証の間に次のプレディケートに検証の経路に沿って前方向に計算する平均のコストを含む、請求項11記載のコンピュータ読み取り可能な記録媒体。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、平均の引き返しの計算コストを使用することを含み、前記平均の引き返しの計算コストは、前記ソフトウェアの検証の間に前のプレディケートに検証の経路に沿って引き返す平均のコストを含む、請求項11記載のコンピュータ読み取り可能な記録媒体。前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、所与の手法により前記受信されたソフトウェアの検証のジョブの実行を初期化するために必要とされる前方向のステップ数と引き返しのステップ数とを使用することを含む、請求項11記載のコンピュータ読み取り可能な記録媒体。1実施の形態では、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定すること、計算ノードの終了の経路の状態を決定すること、及び初期化の経路の状態と終了の経路の状態とに基づいて、計算ノードでの受信されたソフトウェアの検証のジョブの実行を初期化することを含む。初期化の経路の状態は、検証されるべきソフトウェアの開始の状態に到達するためのプログラムのプレディケート叙述関数predicateのシーケンスを含む。受信されたソフトウェアの検証のジョブは、検証されるべきソフトウェアの一部の指示を含む。終了の経路の状態は、計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達した最後の状態の指示を含む。計算ノードは、受信されたソフトウェアの検証のジョブを実行するために割り当てられる。別の実施の形態では、製品は、コンピュータ読み取り可能な記録媒体と、コンピュータ読み取り可能な記録媒体で担持されるコンピュータ実行可能な命令とを含む。命令は、プロセッサにより読取り可能である。命令は、読み取られて実行されたときに、プロセッサに、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定させ、計算ノードの終了の初期化の状態を決定させ、初期化の経路の状態と終了の経路の状態とに基づいて計算ノードでの受信されたソフトウェアの検証のジョブの実行を初期化する。初期化の経路の状態は、検証されるべきソフトウェアの開始の様態に到達するためのプログラムのプレディケートのシーケンスを含む。受信されたソフトウェアの検証のジョブは、検証すべきソフトウェアの一部の指示を含む。終了の経路の状態は、計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達される最後の状態の指示を含む。計算ノードは、受信されたソフトウェアの検証のジョブを実行するために割り当てられる。図1は、ソフトウェアの検証の効率的な並列化を提供する疎結合された分散コンピューティングシステム100の例示的な実施の形態を示す。係る技術は、分散コンピューティングリソース間での効率的なロードバランシングにより提供される。分散コンピューティングシステム100は、複数のネットワーク化された、潜在的なコンピューティングリソースを含む分散コンピューティング環境を含む場合がある。係るコンピューティングリソースは、異なる種類である場合がある。様々な実施の形態では、分散コンピューティングシステム100で実施されるソフトウェアの検証サービスが、近い将来に計算タスクを実行するために特定のトポロジーを利用することができないように、コンピューティングリソースのコネクショントポロジーは、未知であるか又は不規則である。1実施の形態では、分散コンピューティングシステム100は、クラウドコンピューティングのフレームワーク又は環境で実現される場合がある。分散コンピューティングシステム100は、1以上のコンピューティングノードにより実現される。1つの係るコンピューティングノードは、スケジューラノード104として設計及び実現される場合があり、このスケジューラノードは、メインのコンピューティングノードとして機能する。他のコンピューティングノードは、ワーカノード106として設計及び実現される場合がある。コンピューティングノードは、適切なコンピューティングリソース又は電子装置で実現され、限定されるものではないがサーバ、コンピュータ又はそれらの任意の組み合わせを含む。スケジューラノード104は、ワーカノード106に通信可能に結合される。コンピューティングノードは、ネットワーク102を通して通信可能に結合される。ネットワーク102は、コンピューティングノードを通信可能に結合する適切なネットワークアレンジメント、又はワイドエリアネットワーク、ローカルエリアネットワーク、イントラネット、インターネット、又はこれらのエレメントの任意の組み合わせのような適切なネットワークで実現される。分散コンピューティングシステム100は、スケジューラノード104、又は他の適切なサーバ、ノード、又はマシン、或いはその組み合わせから検証のウェブサービス108を実行することで、ソフトウェアの検証の問題の効率的な並列化のサービスを提供する。検証のウェブサービス108のユーザは、検証のウェブサービス108により検査されるべきコード、プログラム、又は他のソフトウェアをロード又はアップロードすることができる。以下では、検査されるべき係るコード、プログラム、又は他のソフトウェアは、検査下にあるコードcodeundertestと呼ばれる。検証のウェブサービス108のユーザは、検証の結果を取得するために検証のウェブサービス108にアクセスすることができる。結果は、以下に記載されるように、分散コンピューティングシステム100で検証のウェブサービス108の動作の出力を含む。コンピューティングノードは、並列に達成されるべきタスクに関連される計算の負荷を共有する。たとえば、検査下にあるコードのようなソフトウェアプログラムの有効性及び動作を検査するために並列して機能する場合がある。係る例では、スケジューラノード104は、検査下にあるコードに通信可能に結合され、検査下にあるコードを検査するためにワーカノード106の動作を編成する。図2は、スケジューラノード104及びワーカノード106のようなコンピューティングノードの例示的な実施の形態を示す。スケジューラノード104は、検査下にあるコード226を動的に試験するため、ワーカノード106に通信可能に結合される場合がある。より多くのワーカノード106がスケジューラノード104に結合される場合があるが、図示されていない。ワーカノード106は、スケジューラノード104からの指示の下で、他のワーカノードと並列して検査下のコード226のようなソフトウェアを検証する。スケジューラノード104は、メモリ218に結合されるプロセッサ220を含む。スケジューラノード104は、スケジューラアプリケーション208を含む。スケジューラアプリケーション208は、プロセッサ220により実行され、メモリ218に記憶されている。スケジューラアプリケーション208は、本実施の形態で記載されるように、スケジューラノード104の動作を実現する。スケジューラノード104は、ジョブのキュー210を含む。ジョブのキュー210は、検証されるべき検査下にあるコード226の一部を表す、1以上のジョブのリストを含む。ジョブのキュー210は、あるキュー又は他の適切なデータ構造で実現される。ジョブキュー210は、メモリ218に記憶されている。スケジューラノード104は、利用可能なリソースのリスト212を含む。利用可能なリソースのリスト212は、検査下にあるコード226の一部を検証するために利用可能な、ワーカノード106のような1以上の計算リソースの一覧を含む。利用可能なリソースのリスト212は、ある表、キュー、又は他の適切なデータ構造で実現される。利用可能なリソースのリスト212は、メモリ218に記憶されている。ワーカノード106は、メモリ222に結合されるプロセッサ224を含む。ノードのプロセッサ220,224は、たとえばマイクロプロセッサ、マイクロコントローラ、デジタルシグナルプロセッサDSP、特定用途向け集積回路ASIC、又は、プログラム命令を解釈及び/又は実行し、及び/又はデータを処理する他のデジタル又はアナログ回路を含む。プロセッサ220,224は、プログラム命令を解釈及び/又は実行し、及び/又は、ノードのそれぞれのメモリ218,222に記憶されるデータを処理する。メモリ218,222は、たとえばコンピュータ読み取り可能な記録媒体といったある期間についてプログラム命令及び/又はデータを保持する任意のシステム、デバイス、又は装置を含む場合がある。ワーカノード106は、ワーカソフトウェアの検証アプリケーション214を含む。ワーカソフトウェアの検証アプリケーション214は、プロセッサ224により実行され、メモリ222に記憶されている。ワーカノード106は、1以上のポリシー216を含み、1以上のポリシーは、検査下にあるコード226の一部の検証における判定を行うために、ワーカノードにより使用される。ワーカノード106は、スケジューラノード104から1以上のポリシー216を受信する。ポリシー216は、限定されるものではないが、ジョブの可用性のポリシー、リソースの可能性のポリシー、及びスケジューリングポリシーを含む。スケジューラアプリケーション208及びワーカソフトウェア検証アプリケーション214は、検査下にあるコード226を検証するような計算のタスクの並列化を可能にするミドルウェアを互いに構成する。ワーカノード106とスケジューラノード104との間の通信は、時間、ネットワーク及び/又は処理リソースの観点で非常に高価である場合がある。分散コンピューティングシステム100は、ワーカノード106とスケジューラノード104との間の通信を最小にする。従って、検査下にあるコード226を検証するタスクは、スケジューラアプリケーション208とワーカソフトウェア検証アプリケーション214を通して、スケジューラノード104とワーカノード106との間で分割される。スケジューラアプリケーション208は、検査下にあるコード226を検証する作業をタスクに分割し、分割されたタスクを並列の検証のためにワーカノード106に供給し、ポリシー及び他の動作パラメータをワーカノード106及び他のワーカノードに供給し、係る並列な検証の結果を得る。ワーカソフトウェアアプリケーション214は、ポリシー216の下でスケジューラノード104により指定されたように、検査下にあるコード226の一部を検査するか、スケージューラノード104により供給される他のパラメータを検査し、その結果を報告する。ノードのプロセッサ220,224は、たとえばマイクロプロセッサ、マイクロコントローラ、デジタルシグナルプロセッサDSP、特定用途向け集積回路ASIC、又はプログラム命令を解釈及び/又は実行し、及び/又はデータを処理する他のデジタル又はアナログ回路を含む。プロセッサ220,224は、ノードのそれぞれのメモリ218,222に記憶されている、プログラム命令を解釈及び/又は実行し、及び/又はデータを処理する場合がある。メモリ218,222は、1以上のメモリモジュールを保持及び/又は収容するシステム、デバイス又は装置を含む。それぞれのメモリモジュールは、たとえばコンピュータ読み取り可能な記録媒体といったある期間についてプログラム命令及び/又はデータを保持するシステム、デバイス又は装置を含む場合がある。図1を参照して、分散コンピューティングシステム100は、分散コンピューティングシステム100でのサービスとして、ソフトウェアの検証108を提供する。ソフトウェアの検証は、分散コンピューティングシステム100の並列の計算能力をてこ入れすることで更に効率的に達成される。1実施の形態では、分散コンピュータシステム100は、記号的実行symbolicexecutionを使用することで、検査下にあるコード226のようなソフトウェアを検証する。記号的実行は、実行における記号の使用により、ソフトウェアの動作を検証するため、適切なやり方で達成される。係る記号的実行がどのように達成されるかに関する1つの例は、米国特許出願12271651のUsingSymbolicExecutiontoCheckGlobalTemporalRequirementinanApplicationsのコピーにおいて発見され、この特許出願の内容は、引用により本明細書に盛り込まれる。記号的実行は、要件をチェックするためにソフトウェアの振る舞いの一部を形式化するために使用される。たとえば、検査下にあるコードの所与の部分の動作は、記号により表現され、プロパティpropertyにより定義される。コードの可能性のある結果が判定される場合があり、係るプロパティは、可能性のある許容可能な値の範囲を示す場合がある。記号的実行は、係るプロパティを無効にする条件が存在するかを判定するために使用される。たとえば、以下のソフトウェアコードを考える。係るコードについて、記号は、コードの様々なエレメントを表現するために使用される。たとえばa=x,b=y,c=zであり、Φは、値及び条件を含めて、結果として得られるセットに等しい。セットΦは、c=abを必要とするコードにおける指示のため、最初にΦ={z=xy}として評価される。次いで、条件文ifc0がコードに現れ、可能性が分割されることを要求する。係る条件文から、zがゼロよりも大きいか否かに依存して、2つの可能性が存在する。従って、セットΦは、Φ={z=xyz>0又はΦ={z=xyz≦0}の何れかとして定義される。2つの係る選択のうちの第一の選択は、zがインクリメントされ、Φ={z=xy1z>1}となることを要求する更なるコードをトリガする。従って、Φ={z=xy1z>1}及びΦ={z=xyz≦0}は、先のソフトウェアコードのフラグメントでの記号的実行を通して計算される、結果として得られるシンボルの経路である。係るコードについて、a>1及びb>0の場合に、cが2よりも大きくなければならないことを要求するプロパティが確立される。係るプロパティは、プロパティを否定し、否定されたプロパティの解が記号的表現に存在するかを判定することで、評価すべき記号的表現に対してチェックされる。たとえば、Φ={z=xyz≦0}について、xは、プロパティにより定義されるように1よりも大きく、yは、プロパティにより定義されるようにゼロよりも大きく、zは、式により必要とされるようにxyに等しく、zは、式により必要とされるように0以下となる必要があり、zは、プロパティを否定することで定義されるように2以下となる必要がある。適切な制約ソルバconstraintsolver又は判定手順decisionprocedureを使用してこれらの式を解くことで、分散コンピューティングシステム100上のワーカノード106は、解が存在しないことを判定し、従ってコードセグメントは、プロパティにより確立される基準をパスする。同様に、Φ={z=xy1z>0}について、xは、プロパティにより定義されるように1よりも大きく、yは、プロパティにより定義されるように0よりも大きく、zは、式により要求されるようにxy1に等しく、zは、式により要求されるように0よりも大きい必要があり、zは、プロパティを否定することで定義されるように2以下である必要がある。適切な制約ソルバ又は判定手順を使用してこれらの式を解くことで、分散コンピューティングシステム100におけるワーカノード106は、解が存在しないことを判定し、従ってコードセグメントは、プロパティにより確立される基準をパスする。係る解が存在する場合、従ってプロパティに違反する場合、係る違反は、バグとして識別される場合がある。係るバグは、分散コンピューティングシステムによりスケジューラノード104に報告され、ログとして記録され、又は最終的にユーザに報告される。コード、特性及びツリーにおけるポイントのような、バグが判定された文脈contextが報告される場合がある。このように、分散コンピューティングシステムは、コードにより実現されるソフトウェアを検証するために検査下にあるコードに記号的実行を行う。検査下にあるコードの記号的実行を行うことで、分散コンピューティングシステムは、自動的な検査を行う。その自動的な検査の間、分散コンピューティングシステムは、検査下にあるコードのそれぞれの条件付き演算で、検査下にあるコードにおける条件付き分岐で使用されるべきデータの可能性のあるセットを表す可能性の範囲を、処理すべき記号的実行のツリーの個別の分岐に分割する。1実施の形態では、係る分岐、分割及び記号的実行は、再帰的に実行される場合がある。図3は、条件に遭遇し、式が評価され、新たなジョブが作成され、バグが決定されたときの、検査下にあるコード226のようなソフトウェアを検証する分散コンピューティングシステム100の動作を例示する。スケジューラノード104は、ジョブをワーカノード106に割り当て、このワーカノードは、STARTノード300で開始する。ワーカノード106は、コードにおける条件文に到達するまで、コードに記号的実行を行う。ある条件文での検査下にあるコード226の記号的実行は、その条件文の後の異なる実行のオプションに関連するコードの記号的実行を必要とする。たとえば、先の例から、ifに関連する条件は、記号的実行が行われるコードの2つの部分を生じる場合がある。あるケースでは、係る2つの部分は、更なる条件を含むコードの大きなセクションを含む。係る2つの部分は、サブツリー302で表現される。記号的実行が行われ且つ検査されるソフトウェア内で遭遇する条件文は、経路の選択ポイント304により表現される。経路の選択ポイント304は、ある条件文の動作を表し、これに対して、複数の後続する経路が可能である。前の例を使用して、ある経路の選択ポイント304のノードは、少なくとも2つの可能なzの範囲を生成し、これに対して、1よりも大きいz、及び0以下のzといった、それぞれの範囲が記号的に実行される。それぞれの係る判定ポイント304は、行われる必要がある更なる条件的な判定を生成する。従って、図3に示されるグラフは、検査下にあるコードの一部の要求される記号的実行の成長を表す。記号的実行の成長により作成されるそれぞれの新たなサブツリー302は、更なる記号的実行を要求するものであり、スケジューラノード104が同じ又は別のワーカノード106に続いて割り当てるジョブとして、ワーカノード106により定義される。結果として、それぞれのジョブは、記号的実行を行うコードのグラフのサブツリー302を表す。図3の例では、4つの条件文が記号的に実行され、ジョブJ1,J2,J3及びJ4として割り当てられている4つのサブツリー302を生成している。スケジューラノード104は、N1,N2,N3及びN4として識別される、1以上のワーカノード106にジョブを割り当てる。ワーカノード106は、検査下にあるコードの記号的実行の間に遭遇されるとき、経路の選択ポイント304の分岐から新たなジョブを定義する。また、ワーカノード106は、検査下にあるコードの記号的実行の間に遭遇されるとき、経路の選択ポイント304の分岐の実行を終了する。たとえば、ジョブJ3の実行の間、ワーカノードN1は、経路の選択ポイントDに遭遇するが、結果として得られる両方の分岐の記号的実行を継続する。対照的に、ワーカノード106は、経路の選択ポイントEに関連する条件文に遭遇し、実行の分岐のうちの1つに関連する少なくとも1つの新たなジョブを作成し、条件文の分岐は、ジョブJ2及びJ4に含まれ、ワーカノードN3及びN2により記号的実行が行われる。新たなジョブを作成、分割及び割り当てたポリシーが以下に説明される。分散コンピューティングシステム100が任意の数のワーカノード106を含むとき、スケジューラノード104によるジョブの割り当てのために任意の数のワーカノード106が利用可能である。スケジューラノード104は、ジョブのキュー210におけるワーカノード106からジョブが作成されたとき、ジョブを記憶する。ワーカノード106は、スケジューラノード104により割り当てられるジョブを記号的に実行する。ワーカノード106は、記号的に実行しているコードにおける更なる条件文に到達する場合がある。以下に記載されるポリシーに依存して、ワーカノード106は、条件文の分岐を処理し続けるか、又は新たなジョブとして条件文の分岐を指定し、新たなジョブをスケジューラノード104にリターンし、この新たなジョブは、以下に記載される基準に従って、スケジューラノード104によりワーカノード106のうちの1つに割り当てられる。ワーカノード106は、以下に記載されるポリシーに依存して、あるジョブの記号的実行を終了する。サブツリー302におけるコードの一部を記号的に実行するワーカノード106は、ある結果に到達し、この結果は、記号的実行により判定されたプロパティに従ってサブツリー302におけるコードの有効性を検証すること、記号的実行により決定されるプロパティの違反としてバグ306を発見すること、或いは、時間、深さ又は別のパラメータの観点で計算の幾つかの境界に到達することを含む。ワーカノード106は、ジョブの終了に応じて、スケジューラノード104に、そのステータス及び記号的実行の結果を伝達する。スケジューラノード104は、ジョブの実行のバランスを取る。作成されたジョブの何れかを実行するために必要とされる作業は、他のジョブに比較して著しく異なる。たとえば、ジョブJ3のサブツリー302は、評価されるべき幾つかのエレメントを含むが、係るエレメントは、ジョブJ2のサブツリー302のエレメントよりもスコープscopeに関してシンプルである。にもかかわらず、1実現では、Xのワーカノード106が利用可能である場合に、所定の数Xのコードのトレースが生成されるまで、スケジューラノード104は、コードのツリーの調査に記号的実行が行われるのを可能にする。従って、深さY1のトレースが多数のワーカノード106に送出され、多数のワーカノード106は、X未満であるか、又はXに等しい。それぞれのワーカノード106がその割り当てられえたジョブを終了したとき、その出力データは、スケジューラノード104に供給され、スケジューラノードは、最後のワーカノード106が終了した後に出力データを収集する。別の実現では、スケジューラノード104は、Xのワーカノード106がコードの一部に記号的実行を行うために利用可能である場合に、少なくともXのトレースが生成されるまで、深さYに記号的実行が行われるように、コードのツリーを調査する。次いで、スケジューラノード104は、ワーカノード106があるジョブを終了するかを判定するため、総当り的なやり方に基づいてワーカノードをポーリングする。所与のワーカノード106が終了した場合、スケジューラノード14は、ジョブの出力を収集し、丁度終了したワーカノード106に、ジョブのキュー210からの新たなジョブを送出する。しかし、係る実現は、他のジョブよりも大きいジョブを考慮していない場合があるか、幾つかのワーカノード106は、他のワーカノード106が大きなジョブで作業している間に使用されていない場合がある。係る実現は、あるジョブを動的に分割し、係る分割されたジョブを使用されていないワーカノードに割り当てるように構成されていない。動作において、1実施の形態では、スケジュールノード104は、ジョブが作成されたとき、及び記号的実行が行われたときに、ジョブを知的且つ動的に釣り合いを取る。図4は、記号的実行が行われるコードを知的且つ動的に区分する分散コンピューティングシステム100の動作を例示する。グラフ402は、コードに記号的実行が行われ、新たなジョブが作成され、終了の状態に到達したとき、検査下にあるコードの実行ツリーを例示するものであり、スケジューラノード104の指示の下でワーカノード106によりバグが発見される。スケジューラノード104は、以下に記載されるポリシー及び方法を使用して、あるジョブをワーカノード106に割り当てる。グラフ402は、ワーカノード106によりジョブの記号コードの実行を表す。ワーカノードがジョブの記号的実行を開始する最初の実行ポイント404は、初期化の経路の状態に対応する。初期化の経路の状態は、最初の実行ポイント404に導かれる条件文の一連の決定又は値を含む。初期化の経路の状態は、ジョブがワーカノード106に割り当てられたとき、スケジューラノード104により設定される。ワーカノード106は、初期化の経路の状態において記録される決定の再生を通して初期化される。初期化の経路の状態は、最初の実行ポイント404に導かれる検査下にあるコードにおける実行のツリーまでの条件付き判定のレコードである。ワーカノード106は、幾つかの条件のうちの1つに到達するまで、コードに記号的実行を行う。はじめに、ワーカノード106は、その分岐が検証されるまでツリーの分岐に記号的実行を行い、記号的実行は、バグ又はエラーを検出することなしに、その分岐について終了する。係る条件は、検証されたポイント414により表現される。検証されたポイント414は、検証されたプログラムの振る舞いのトレースを表す。第二に、ワーカノード106は、ある条件文でツリーの分岐に記号的実行を行い、このツリーは、1以上のサブツリーに処理される。それぞれのサブツリーは、後になって記号的実行の新たなジョブとして記号的に実行されるか又はマークされる。係るポイントは、実行されたポイント408により表現される。第三に、上述されたように、ワーカノード106は、1以上の新たなジョブが記号的実行の結果として作成されるまで、ツリーの分岐に記号的実行を行う。割り当てのためにスケジューラノードに送出される、新たなジョブとしてのサブツリーの係る部分の指定は、以下に記載されるポリシー及び方法に従って、ワーカノード106により行われる。係る条件は、新たなジョブ410により表される。第四に、グラフの一部は、記号的実行が施され、記号的実行により判定されたときに、バグ、矛盾、又は他のエラーを含むことが判定される。係るバグは、スケジューラノード104に送出される。バグは、グラフ402上のバグ414として表現される。あるジョブの終了に応じて、ワーカノード106は、終了の経路の状態を記憶する。終了の経路の状態は、ジョブが終了されたとき、ワーカノード106が実行していた状態を反映する。終了の経路の状態は、その状態に到達するために必要なプレディケートステップpredicatestepのレコードを含む場合がある。終了の経路の状態は、ワーカノード106が将来において所与のジョブについて良好なフィットであるかを判定するために使用される。図1及び図2を参照して、分散コンピューティングシステム100は、コードを効率的に解析するため、ワーカノードの間で処理ジョブの負荷を知的且つ動的に釣り合いを取るために知的な判定intelligentdecisionを行うために、1以上のポリシーを使用する。スケジューラノード104は、割り当てられるジョブと共に係るポリシーをワーカノード106に割り当てるか、スケジューラノード104の動作においてポリシーを実現する。ワーカノード106は、スケジューラノード104と更なる通信を行うことなしに、ポリシーを実行する。1実施の形態では、分散コンピューティングシステム100は、現在のジョブ内でサブツリーに記号的実行を行い続けるワーカノード106とは対照的に、ワーカノード106が、コードのサブツリーに記号的実行を行っている間に、将来の処理のために係る新たなジョブを何時生成すべきかを判定するため、ジョブの可用性のポリシー216aを使用する。別の実施の形態では、分散コンピューティングシステム100は、あるジョブに記号的実行を行っている所与のワーカノード106が、そのジョブに記号的実行を行い続けるのではなく、そのジョブの記号的実行を何時終了すべきか、新たなジョブの割り当てのために何時利用可能となるかを判定するために、リソースの可用性のポリシー216bを使用する。更に別の実施の形態では、分散されたコンピューティングシステム100は、スケジュールノード104により、ジョブのキュー104におけるどのジョブが、利用可能なリソースのリスト212において指定されたどのワーカノード106に割り当てられるべきかを判定するため、スケジューリングのポリシー216cを使用する。上述されたように、スケジュールノード104は、知的且つ動的なロードバランスを通してソフトウェアの解析を効率的に並列化するため、分散コンピューティングシステム100の動作を調整する。スケジューラノード104は、検査下にあるコードの記号的実行を初期化し、ワーカノード106をジョブに割り当て、ワーカノード106からの結果及び新たなジョブの戻りをモニタし、ワーカノード106をジョブキュー210からの更なるジョブに割り当て直し、ワーカノード106の実行及び終了を調整し、検査下にあるコードの記号的実行が何時終了するかを判定する。スケジューラノード104は、結果、新たに識別されたジョブ、ステータス及びパラメータをやり取りするためにワーカノード106と通信する。1実施の形態では、スケジュールノード104は、ワーカノード106がコードに記号的実行を行っている間に、ワーカノード106のパラメータを更新する。係る更新は、ワーカノード106から受信された、実行の統計量を含む状態に基づいており、ワーカノード106は、スケジューラノード104に、ジョブの実行が期待されたよりも長く要するか又は短く要するか、所定数の新たなジョブが生成されているか又は所定の割合で生成されているか、実行が所定の時間長について生じているか、或いは他の適切な情報を通知する。スケジューラノード104は、そのワーカノードから受信された情報に基づいて、個々のワーカノード106についてジョブの可用性のパラメータ又はリソースの可用性のパラメータを調節する。スケジューラノード104は、ワーカノード106からの集合の状態の報告に基づいて、或いは、ジョブキュー210又は利用可能なリソースのリスト212の状態に基づいて、ある範囲のワーカノード106についてジョブの可用性のパラメータ又はリソースの可用性のパラメータを調整する。図5は、知的且つ動的なロードバランシングを通してソフトウェアの解析を効率的に並列化するため、分散コンピューティングシステムの動作を調整する方法500の例示的な実施の形態である。1実施の形態では、本方法500は、スケジュールノード104により実現される。他の実施の形態では、本方法500は、ワーカノード106により部分的に実現される。ステップ505で、最初の記号的実行の段階が達成される。適切な初期化が使用される場合がある。1実施の形態では、検査下にあるコードのXの初期化シーケンスが発見及び作成される。初期化シーケンスは、検査下にあるコードの実行ツリーにおける最初の実行ポイントを反映する。それぞれが異なるワーカノードに対応するX個の異なる最初の実行ポイントを十分に作成するため、幾つかの記号的実行が行われる場合がある。X個の最初の実行ポイントの数は、利用可能なワーカノードの数よりも多くあるべきである。利用可能なリソースリストは、利用可能なワーカノードの数を決定するために調べられる。ステップ507で、それぞれの初期化シーケンスのジョブは、ジョブのキューに追加される。ステップ510で、N個のワーカのどの動作が開始される。N個のワーカノードの動作を開始する適切な方法が使用される場合がある。1実施の形態では、スケジューリングポリシーは、ジョブのキューからの未解決のジョブをワーカノードに割り当てるために調べられる。別の実施の形態では、ワーカノードの数Nは、未解決のジョブの数Xよりも少ない。それぞれのワーカノードについて、ステップ515で、入力パラメータは、ワーカノードに供給される。係る入力パラメータは、ジョブの可用性のポリシー又はリソースの可用性のポリシーのようなポリシーから導出される。係るポリシーは、どのような条件下で新たなジョブが作成されるべきか、及び記号的実行が何時終了されるべきかに関するワーカノードの情報を供給する。ステップ520で、ジョブのキューと利用可能なリソースのリストがモニタされる。ステップ525で、ジョブ及び利用可能なリソースの両者はジョブのキューと利用可能なリソースリストにおいて未解決であるかが判定される。未解決である場合、ステップ530で、あるジョブが利用可能なワーカノードに割り当てられる。そのようにするため、スケジューリングポリシーは、どのジョブをどのワーカノードに割り当てるべきかを判定するために使用される。ステップ535では、入力パラメータは、ワーカノードに供給される場合がある。係る入力パラメータは、ジョブの可用性のポリシー又はリソースの可用性のポリシーのようなポリシーから導出される。係るポリシーは、どのような条件下で新たなジョブが作成されるべきか、及び記号的実行が何時終了されるべきかに関するワーカノードの情報を提供する。ステップ537で、余りに多くのジョブ、十分ではないジョブ、余りに多くのリソース又は十分ではないリソースが未解決である場合、ジョブの作成又はリソースの可用性を統括するポリシーが評価し直される場合がある。利用可能なリソースなしでジョブが未解決である場合、リソースの使用を良好に最大にするため、ポリシーは調べられ、調節される。たとえば、ジョブの可用性のポリシーは、記号的実行の間により少ない新たなジョブを作成するために調整される場合がある。リソースの可用性のポリシーは、ワーカノードにより記号的実行をすみやかに終了するために調整される。同様に、利用可能なワーカノードがジョブなしで未解決である場合、ポリシーが調べられ、調整される。たとえば、ジョブの可用性のポリシーは、記号的実行の間の更なる新たなジョブを作成するために調節される。リソースの可用性のポリシーは、ワーカノードによる記号的実行を延長するために調節される。ステップ540で、記号的実行が終了されるべきかが判定される。係る判定は、適切なやり方で行われる。1実施の形態では、ジョブのキューが空であるか、そして全てのワーカノードが使用されていないかが判定される。ジョブのキューが空であって、全てのワーカノードが使用されていない場合、この条件は、検査下のあるコードの記号的実行が終了されていることを示す。記号的実行が終了している場合、ステップ545で、ワーカノードによる記号的実行からの全ての結果が収集され、結果が記憶され、ワーカノードが終了される。ステップ550で、検査下にあるコードの記号的実行が終了されていない場合、何れかのワーカノードが、それらの割り当てられたジョブを実行することから回復しているかが判定される。係る判定は、適切なやり方で行われる。1実施の形態では、あるジョブで終了したワーカノードは、そのジョブの終了に関する通知を提供する。ステップ555では、ワーカノードにより前のジョブの実行の間に作成された新たなジョブは、ジョブのキューに追加される。ステップ560で、ワーカノードは、分散コンピューティングシステムにおいてソフトウェアを検証し続ける場合に、利用可能なリソースのリストに戻される。幾つかのワーカノードは、分散コンピューティングシステムの一部として、記号的実行のためにもはや利用可能ではなく、従って利用可能なリソースのリストに戻されない。ステップ565では、検査下のあるコードの記号的実行が終了されていない場合、コードの記号的実行が終了するまで、ステップ525における未解決のエントリについてジョブのキュー及び利用可能なリソースのリストをモニタするステップが繰り返される。図4を参照して、ワーカノード106は、スケジューラノード104により、あるジョブが割り当てられる。ワーカノード106は、永続的なやり方で又は新たに割り当てジョブに関連して、スケジューラノード104から、1以上の動作パラメータを受信する。動作パラメータは、ワーカノードにより記憶される、1以上のポリシーに基づいている。ワーカノード106は、終了の状態に到達するまで、ジョブに関連されるソフトウェアを解析する。ワーカノード106は、適切なやり方でソフトウェアを解析する。1実施の形態では、ワーカノード106は、ソフトウェアに記号的実行を行う。終了の状態は、リソースの可用性のポリシーに基づいている。解析の間、ワーカノード106は、コードを解析している間に発見された検査下にあるコードにおいて発見された分岐から新たなジョブを作成する。ワーカノード106が新たなジョブを作成する条件は、検査下にあるコードの一部を解析し続けるのとは対照的に、ジョブの可用性のポリシーに基づいている。ワーカノード106は、新たなジョブを含めて、検査下にあるコードを解析した結果をスケジューラノードに送出する。ワーカノード106は、利用可能なリソースのリスト212に戻り、更なる割り当てられたジョブを待つか、又は、ソフトウェアを解析する分散ネットワークシステム100に参加することができない場合に、利用可能なリソースのリスト212に戻らない。ワーカノード106による計算の終了に応じて、ワーカノード106は、その最後の既知の状態を保持する。係る最後の既知の状態は、計算が終了したときに記号的実行を行っていた経路を含む。係る経路は、終了の経路の状態として知られている。終了の経路の状態は、新たなジョブ及び新たなノードの初期化を新たに終了したワーカノード106に割り当てるため、スケジュールノード104のスケジューリングポリシーの一部として使用される場合がある。図6は、分散コンピューティング環境におけるソフトウェアの解析の問題の並列化のための効率的な部分的計算の方法600の例示的な実施の形態である。1実施の形態では、本方法600は、1以上のワーカノード106により実現される。本方法600は、任意の数のワーカノード106により並列に行われる。別の実施の形態では、本方法600は、スケジューラノード104により全体的又は部分的に実現される場合がある。本方法600は、図5のステップ510及び530の実行に応じて開始される。ステップ605では、利用可能なリソースのリストが結合される。係るリストを結合することは、ソフトウェアの一部を解析する新たなリソースの可用性に関して直接的又は間接的な通知をスケジューラノードに提供する。ステップ610では、解析されるべきソフトウェアの一部に対応するジョブが受信される。同時に、解析の動作に関するパラメータが受信される。係るパラメータは、割り当てられたジョブの一部として提供される。係るパラメータは、初期化の経路、初期化の経路の状態、サーチストラテジ、ジョブの可用性のポリシー、リソースの可用性のポリシー、又は他の適切な動作パラメータを含む。1実施の形態では、ポリシーは、予め受信される場合がある。ステップ615では、初期化のシーケンスが再生される。初期化のシーケンスを再生することは、初期化の経路に対応する動作のセットを行うことを含む。初期化のシーケンスを再生した結果、検査下のあるコードの解析の開始ノードに到達する。ステップ615で、検査下のあるコードの最初の解析の適切なやり方が使用される。1実施の形態では、最初の再生は、計算及び解析について初期化するために使用される。別の実施の形態では、計算及び解析を初期化するため、部分的な引き返しbacktracking及び再生replayが使用される。初期化の再生は、実行及び再生のツリーの開始で、検査下にあるコードの記号的実行の間に行われたそれぞれの条件文の判定を開始することを含む。部分的な引き返し及び再生は、前のワーカノードの終了の経路の状態を決定すること、コードにおける条件付き分岐に関連するサブツリーにおいて高い幾つかの判定を取り消すことundoingを含む。係る終了の経路の状態は、割り当てられたジョブがパラメータとして提供される。1以上の前の実行が取り消される場合があり、従って実行の経路は、更なる条件付き判定が再生されるツリーにおける前の高いポイントに部分的に引き返される。ステップ620で、検査下にあるコードは、記号的実行が行われるか、さもなければ解析される。解析されるコードは、初期化の経路の状態に最初に対応する。本方法600の動作の間、ステップ620は、ジョブに対応する検査下にあるコードの実行ツリーの複数の部分について行われる。1実施の形態では、ステップ620は、検査下にあるコードにおける分岐点に到達するまで継続する。係る分岐点は、検査下にあるコードにおける条件文を含み、これに対して、子の実行ツリーが生成され、続いて記号的実行が行われ又はさもなければ解析される。どの分岐を実行すべきか及び記憶すべきかに関する判定は、選択されたサーチストラテジに依存する。適切なサーチストラテジが選択される。1実施の形態では、深さ優先のストラテジが使用され、実行ツリーにおけるより深い進出が好まれ、従ってより深い進出につながる分岐が選択される。別の実施の形態では、分岐優先のストラテジが使用され、実行ツリーのより広い拡大がより深い進出よりも好まれる。更に別の実施の形態では、最良優先のストラテジが使用され、幾つかの特定の動作パラメータを使用して分岐が選択される。たとえば、分岐のタイプは、好まれる所与の重要度、実行の速度又は他の基準である。分岐点に到達しない場合、実行ツリーにおける葉のノードに到達するまでステップ620は継続し、検査下にあるコードのサブツリーが完全に解析される。係る解析されたサブツリーは、矛盾又は他のエラーのインジケータが発見された場合に、サブツリーはバグを含むという結論に繋がる。別の場合、係る矛盾又は他のインジケータが発見されない場合、サブツリーが検証されたと判断される。ステップ625で、分岐点に到達する。1実施の形態では、1つの分岐は、更なる記号的実行により調査され、他の分岐は、調査されていない分岐として記憶される。別の実施の形態では、全ての分岐は、調査されていない分岐として記憶される。調査されていない分岐を記憶するため、初期化のシーケンス、又は分岐につながるステップが記録される。1実施の形態では、調査されていない分岐に関連する新たなジョブは、検査下にあるコードの記号的実行の間に作成される。係るケースでは、本方法600は、ステップ630、続いてステップ640に進み、調査されていない分岐から新たなジョブが作成される必要があるか、終了の閾値に到達したかを判定するためにポリシーが評価される。別の実施の形態では、調査されていない分岐に関連する新たなジョブが記号的実行の終了でのみ作成される。係るケースでは、調査されていない分岐から新たなジョブを作成し、作成された新たなジョブをジョブのキューに追加するステップは、ステップ650に関連してのみ行われる。ステップ630では、ジョブの可用性のポリシーは、調査されていない分岐が解析のための新たなジョブとして指定されるべきか、又は本方法600の現在のインスタンスinstance内の調査のために保持されるべきかを判定するために評価される。ジョブの可用性のポリシーは、最近判定された調査されていない分岐について、及び前に判定された調査されていない分岐について評価される。適切なジョブの可用性のポリシーが使用される場合がある。ジョブの可用性のポリシーは、現在のジョブについて実行がどの位長く実行が続いているかに関する判定を含む。新たなジョブを作成する判定により、記号的実行のサブツリーへの分割が引き起こされ、検査下にあるコードにおける条件付き判定に関連する分岐が、分離され、新たなジョブが形成される。ジョブの可用性のポリシーの更なる実施の形態は、以下に説明される。ステップ632で、解析のための新たなジョブとして調査されていない分岐を指定するような動作について、ジョブの可用性のポリシーにより動作が要求される場合、ステップ635で、調査されていない分岐は、新たなジョブとしてジョブのキューに配置される。1実施の形態では、新たなジョブのジョブのキューへの実際の配置は、即座に開始される。係るケースでは、新たなジョブは、スケジューラノードに転送される。別の実施の形態では、新たなジョブのジョブのキューへの実際の配置が遅延される。係る遅延は、スケジューラノードによる要求に応じて、又はリソースの可用性のポリシーに従って現在のジョブの早期の終了に応じて、クリティカルな数の新たなジョブが作成されるまで、ある時間の間隔を含む。さらに、ステップ635で、新たなジョブを生成したサーチストラテジの文脈を示す部分的なサーチパラメータが記憶される。ステップ640で、リソースの可用性のポリシーは、ジョブが未だ完全に解析されていないとしても、ジョブの解析が終了すべきかを判定するために評価される。適切なリソースの可用性のポリシーが使用される場合がある。可能性のあるリソースの可用性のポリシーが以下に説明される。ステップ645で、ジョブの計算及び解析が終了すべき場合、ステップ650で、新たなジョブが残りの調査されていない分岐についてジョブのキューで作成され、ステップ652で、部分的なサーチパラメータが記憶される。ステップ650は、ステップ635に類似したやり方で実現される。ステップ655で、ジョブが終了される。最後の解析の状態及び位置が記憶される。係る状態及び位置は、将来の初期化のポイントの基準としての役割を果たす。解析の結果、新たなジョブ、及び他の収集された情報は、スケジューラノードに供給される。使用されていないこと及び更なるジョブの要求を示す利用可能なリソースのリストが結合される。ジョブの計算及び解析がジョブの可用性のポリシーにより終了することが判定されていない場合、ステップ600で、実行のツリーが評価される。実行ツリーは、適切なやり方で評価される場合がある。1実施の形態では、実行ツリーは、上述されたサーチ問合せに従って評価される。実行ツリーが使い尽くされた場合、ステップ670で、ジョブが完了され、本方法はステップ652に進む。実行ツリーが使い尽くされていない場合、本方法は、ステップ620に進み、コードの記号的実行を継続する。ステップ620が記号的実行を開始する実行ツリーにおける位置は、上述されたサーチストラテジに従って決定される。本方法600の実行の間、実行の長さ、作成される新たなジョブ、調査される分岐、使用されるサーチパラメータ、又は他の情報に関するステータスのアップデートがスケジューラノードに送信される。本方法600の実行の間、動作パラメータがスケジューラノードから受信される。1実施の形態では、係るパラメータは、たとえばステップ610で記載されるように、1度だけ受信される。別の実施の形態では、動作パラメータは、スケジューラノードから間欠的に受信される。係る実施の形態では、係るパラメータは、本方法600の動作を変更するために組み込まれる。図4を参照して、ワーカノード106は、分散コンピューティング環境でソフトウェアの解析の問題の効率的な並列化のための動的且つ知的な部分的な計算の管理を提供する。ワーカノード106は、解析、記号的実行、又は知的且つ動的に境界が付けられる計算により係るタスクを達成する。1実施の形態では、ワーカノード106は、解析の文脈におけるファクタに基づいて、境界付けされた解析の閾値を適用する。先に示されたように、所与のワーカノード106による解析は、たとえばジョブの可用性のポリシーとリソースの可用性のポリシーに関連されるパラメータにより制御される。係るパラメータは、スケジューラノード104により伝達される。ジョブの可用性及びリソースの可用性の両者は、新たなジョブを作成するために条件付き分岐に基づいて所与のワーカノード106が所与のジョブを何時分割すべきかを判定するために使用されているとき、及び/又は所与のワーカノード106がそのジョブを計算するのを何時終了したかを判定するために使用されているとき、といった様々な要素を考慮する。係る要素は、境界関数で評価される。1実施の形態では、係る要素は、限定されるものではないが、以下を含む。1現在行われている実行のツリーの深さ-x;2所与のサブツリーの実行に費やされる時間-y;3所与のサブツリーで調査される判定ノードの数-z;4利用可能なリソースのリストにおいて使用されていないフリーのリソースの数-w;及び5ある経路上の平均時間-u及び終了された経路-vの平均の深さ、のようなグローバルなレベルでの計算の履歴及び/又は統計量。境界関数におけるこれらのエレメントの組み合わせは、ある閾値に比較される。ワーカノード106は、閾値を超えるか又はさもなければ閾値に合致する境界関数の結果により閾値がトリガされているかを判定する。係るケースでは、新たなジョブが作成されるか、又はそのケースでは、ワーカノードは、その計算を終了する。係る閾値は、上述されたパラメータの適切な組み合わせにより決定される。使用される閾値は、ジョブの可用性のポリシーとリソースの可用性のポリシーとの間で異なる。閾値は、それぞれの係るポリシーについて、検査されるべきコードの特定のタイプ、及び検査されるべき特定のコードのセットについて実験的に決定される場合がある。閾値は、新たなジョブの作成及びワーカノードの計算との釣り合いを取るために、実験的に決定される場合がある。上述されたパラメータのそれぞれには、対応する定数又はa,b,c,d,e又はfのような重み付け値が割り当てられる。従って、係る閾値Tを超えているかに関する判定は、以下の境界関数の例となる式により形式化される。axbyczdweufv>T境界関数は、たとえば1以上の上述されたパラメータを使用して閾値を超えているかを判定するため、適切な計算又は判定を使用する。たとえば、複雑な論理式、2変数関数、非線形関数、又はファジー計算が境界関数として使用される。たとえば、待機しているワーカノードの数が10を超えた場合、ジョブの可用性の閾値は、他の要素に係らず、自動的に超えられる。別の例では、ジョブは、シンプルに終了され、全ての発見された新たなジョブを解放する。更に別の例では、待機しているワーカノードに対応する要素の重み付け値が増加される。係る例は、ジョブのキュー又は利用可能なリソースのリストがある最大値を超えたか、又はある最小量よりも下回ったかを調べることでトリガされる。係る制約は、閾値Tについて記載された実験に類似した実験により決定される。より大きな重み又はより小さな重みは、それらの影響が特定の状況において決定されたとき、所与のパラメータに配置される場合がある。たとえば、スケジュールノード104は、制約を調節し、従って、ワーカノード106からのステータスのアップデートに基づいて、利用可能なリソースのリスト212におけるリソースの可用性に基づいて、又はジョブのキュー210における新たなジョブに基づいて、関連されるポリシーを調節する。スケジュールノード104は、ジョブのキュー210における未解決のジョブに関連してワーカノード210の使用を最適化するため、係る制約を調節する。同様に、スケジュールノード104は、リソースの可用性のポリシー又はジョブの可用性のポリシーの何れかに関連する閾値を調節する。ジョブの可用性のポリシーの閾値は、リソースの可用性の閾値よりも低い。係るケースでは、ワーカノードが終了されていない間に、ジョブが生じる。さもなければ、閾値が等しい場合、現在のジョブの実行の終了と同時に新たなジョブが生じる。1つの例では、新たなジョブを作成する閾値関数は、以下の式となるように決定される。-5x0.02y0.005z10w-0.01u-1v>50この閾値関数を超えて、ワーカノード106により遭遇される調査されていない分岐は、新たなジョブとして作成される。制約の値は、唯一の例を反映しており、特定のソフトウェアの解析で遭遇される特定の状況に依存して変化する。相対的な重み及びそれぞれの極性の議論は、例について以下に与えられる。-5xxは、実行が行われている計算ツリーの深さである。深さは、それぞれの記号による分岐のレベルで1だけ増加する。従って、計算が行われているツリーの深さが増加するときに、再生の非常に高いコストが、閾値に到達して新たなジョブを開始することが困難となることを意味するとき、定数aは、負である可能性がある。0.02yyは、ワーカノード106が現在のジョブに関して計算している時間秒である。係る解析により費やされる時間が多くなると、解析を終了して、新たなジョブを生じる傾向が高くなることを意味する。従って、定数bは、典型的に正の値である。0.005zzは、サブツリーで既に遭遇された判定ノードの数である。判定のサブツリーが余りに大きくなり過ぎた場合、ジョブを終了し及び/又は新たなジョブを生じる傾向が増加する。従って、定数cは、典型的に正である。サブツリーにおいて既に遭遇した非常に多くの判定ノードが、動的にバランスを取る必要がある作業負荷の程度に関して重要ではないとき、cの値は、比較的低い。10wwは、利用可能なリソースのキューにおける使用されていないワーカノード106の数である。使用されていないワーカノードは、有すべき非常に悪い問題であり、係るように、定数dは、正であって且つ大きい。大きな数は、既存のジョブをすぐに終了すると同様に、より積極的に新たなジョブに広がる。新たなジョブは、現在実行しているジョブの終了までジョブのキューに追加されないリソースの可用性のポリシーの文脈では、係る定数は、ジョブのキューへの追加のために新たなジョブを解放するように非常に高い。係る状況では、ワーカノード106により発見される未解決の新たなジョブの数は、この要素を考慮する。-0.01uuは、ある経路に関する平均時間秒である。これは、現在のジョブ内の経路の平均時間であるか、又はスケジューラノード104により集められた全てのジョブにわたる平均時間である。この要素は、幾つかの有効な作業を完了するための最少の時間量を確定するか、又は、新たなジョブの頻繁な非生産的な発生を防止するために使用される。係るように、定数eは、負であり、分散ネットワークシステム100の速度に従って比較的小さい。この要素は、ジョブをワーカノード106に割り当てるオーバヘッド、及びワーカノード106とスケジュールノード104との間の通信のために性能が低下する、リソースの過剰なチャーニングchurning、又は過剰な小さく且つ実体のないジョブの過剰な発生を防止するために使用される。-1vvは、ワーカノード106によりこれまでの遭遇した解析及び実行の経路の平均の深さである。これは、現在のジョブ内の経路の平均、又はスケジューラノード104により集められる全てのジョブの平均である。この要素は、所定の深さに到達したかを判定するために使用され、所定に深さに到達した場合に、新たなジョブを生じる。幾つかのケースでは、この要素は、深い実行のレベルを促進するために使用される。従って、定数fは、正又は負である。>50上述されたように、ジョブの可用性及びリソースの可用性の閾値は、それぞれ、個別に又は一緒に決定される。スケジューラノード104は、ワーカノード106の使用を比較的最適にする要件に依存して、ワーカノード106について何れかの閾値を調節する。ジョブの可用性及びリソースの可用性の閾値は、互いに関して調節される。図7は、分散コンピューティング環境でのソフトウェアの解析の問題の効率的な並列化のための動的且つ知的な部分的な計算の管理の方法700の例となる実施の形態である。1実施の形態では、本方法700は、1以上のワーカノード106及び/又はスケジューラノード104により実現される。ステップ705では、ソフトウェアの解析の範囲の境界をつけるパラメータが設定される。1実施の形態では、係るパラメータは、スケジューラノードから受信される。別の実施の形態では、係るパラメータは、ワーカノードに送出される。最適なパラメータは、適切な動作パラメータを含む場合がある。1実施の形態では、パラメータは、閾値を含む。別の実施の形態では、パラメータは、重み付けされた値を含む。動作パラメータは、ソフトウェアの解析の適切な態様に関する。動作パラメータは、1実施の形態では、動作パラメータは、ジョブの可用性のポリシーに関する。別の実施の形態では、動作パラメータは、リソースの可用性のポリシーに関する。パラメータは、適切な形式を有する場合がある。1実施の形態では、パラメータは、式axbyczdweufv>Tを有する。ステップ710で、動作の要素が決定され、これらの要素は、ソフトウェアの記号的実行に関連する。係る動作の要素は、計算が行われているツリーの1以上の深さ、サブツリーにおける計算で費やされる時間、サブツリーで調査される判定ノードの数、リソースのキューにおいて使用されていないフリーのリソースの数、実行の経路で費やされる平均時間、及び/又は完了された実行経路の平均の深さを含む。ステップ715で、記号的実行に関連する動作のポリシーが評価される。係る評価は、たとえば、検査下にあるコードにおける調査されていない分岐の発見、ジョブの終了、又はサブツリーの完了に応じてトリガされる。ステップ715は、たとえばステップ630及び640で実現される。動作のポリシーは、たとえばジョブの可用性のポリシー又はリソースの可用性のポリシーを含む。ステップ720で、ステップ715に関連して、動作ポリシーに関連する閾値を超えたかが判定される。係る閾値は、ステップ705において境界付けるパラメータのセットに従って設定され、境界付けるパラメータ及びステップ710で決定された動作の要素に従って判定される。閾値を超えている場合、ステップ725で、動作が行われる。係る動作は、現在のジョブの記号的実行を終了すること、又は新たなジョブを生じることを含む。ステップ730で、ワーカノードのような使用されていないリソースの数、及び実行されるべき未解決のジョブの数が評価される。ステップ735で、未解決のジョブが僅かであるか又は全くない一方で、多くのワーカノードが使用されていない場合、ステップ740で、境界付けパラメータは、新たなジョブの発生を増加するために調節される。同様に、境界付けパラメータは、既存のジョブの記号的実行の終了を減少するために調節される。ステップ745で、使用されていない状態のワーカノードが僅かであるか又は全くない一方で、多くのジョブが未解決である場合、ステップ750で、境界付けパラメータは、既存のジョブの記号的実行の終了を増加するために調節される。同様に、境界付けパラメータは、新たなジョブの発生を減少するために調節される。本方法は、現在実行されているジョブが終了されるまで、ステップ710で繰り返される。図4を参照して、ワーカノード106は、分散コンピューティング環境におけるソフトウェアの解析の問題の効率的な並列化のためのノードの計算の初期化技法を適用する。同様に、スケジューラノード104は、スケジューリングポリシーを評価するとき、係るノードの計算の初期化技法を適用する。ひとたびワーカノード106が特定のジョブが割り当てられるために選択されると、ワーカノード106は、記号的実行のためにその計算を初期化する。係る初期化は、実行のために初期状態404を設定するための1以上の初期化のオプションの間で選択することを含む。特定の初期化のオプションを選択することは、初期化の間に記号的実行を迅速化する。異なる初期化のオプションの可用性は、特定のジョブについて様々な利用可能なワーカノード106の初期化の要件を考慮するとき、スケジューラノード104のスケジューリングのポリシーに影響を及ぼす。ノードの計算の初期化を記述する注記は、指示のプレディケートdenotingpredicatesを含む。検査下にあるコードは、任意の数のプレディケート又はプログラム変数を含む。たとえば、プレディケートは、ν1<5ORν2=Trueであり、ν1及びν2はコードにおける変数である。係るプレディケートは、P1,P2等として示される。経路の条件は、記号的実行の状態を表現するために使用される、プログラムのプレディケートの順序付けされたシーケンス、又はそれらの否定を含む。たとえば、P1,¬P2,P4,¬P7,P9は、それぞれの判定ポイントでこれら5つのプレディケート又はそれらの否定を選択することで到達されるプログラムの記号的実行のツリーにおけるあるポイントを表す。初期化の経路の状態IPCは、特定の記号の実行経路に関連され、ジョブが初期化される必要がある経路の状態を表す。ワーカノード106は、IPCから記号的実行を始める。IPCの例は、初期化のポイント404に到達するために記号的実行の間に行われる判定のシーケンスである。終了の経路の状態TPCは、特定のワーカノード106と関連付けされ、ワーカノード106での記号的実行が終了される最後の経路の状態を表す。TPCは、ワーカノード106が処理した前のジョブからのワーカノード106での記号的実行の最後の状態を表す。TPCの例は、終了の経路の状態412である。ワーカノード106は、あるジョブの終了に応じてそのTPCを記憶する。スケジューラノード104は、初期化コストの計算の一部として、ジョブをワーカノード106に割り当てるとき、ワーカノード106のTPCを考慮する。1つの係る初期化のオプションは、完全な再生であり、ワーカノードの計算は、ジョブに関連する条件文の全ての判定を再生することで初期化される。係るオプションは、記号の経路に沿ったプログラムの前方向の計算を含む。係るオプションは、検査下にあるコード内の条件文に関する前の判定を再生する余分のリソースを必要とする。ワーカノードの計算の初期化のための別のオプションは、引き返し及び再生であり、終了の経路の状態における条件文に関連する前の判定が取り消される。共通のプレディケートのセットに到達するために必須の数の前の判定が引き返された後、ジョブの初期化の経路の状態に従ってノードが初期化されるまで、他のプレディケートの判定が再生される。TPCから開始して、プレディケートは、経路の条件が所望のIPCのプレフィックスと同じになるまで、一度に引き返された1つのプレディケートである。次いで、所望のIPCが達成されるまで、IPCの残りのステップは、前方向に再生される。図8は、例となる初期化の経路の状態及び終了の経路の状態に関する完全な再生、並びに、引き返し及び再生の動作を示す。たとえば、利用可能なリソースに割り当てられるべきジョブのキュー210における特定のジョブは、{P1,¬P2,P4,¬P7,P9}の初期化の経路の状態を有する。係るジョブは、前のジョブを実行することからの、その終了の経路の状態が{P1,¬P2,P4,¬P7,P11,¬P14}である利用可能なリソースのリスト212におけるワーカノード106について評価される。従って、ジョブの初期化の経路の状態とワーカノード106の終了の経路の状態の最初の4つのエレメントは、同じである。完全な再生の初期化のオプションを利用して、候補となるワーカのノード106は、{P1,¬P2,P4,¬P7,P9}のプレディケートの判定を行うことで、ジョブの初期化の経路の状態の全てのエレメントの実行を再生することが必要とされ、そのようにするために5つのステップを要する。引き返し及び再生のオプションを利用して、候補となるワーカノード106は、{¬P14,P11}のプレディケートの動作をはじめに引き返し、次いで、未解決のジョブの初期化の経路の状態に整合するようにP9の動作を再生し、全体として3つのステップを必要とする。この特定の例では、バックトラックアンドリプレイのオプションは、未解決のジョブの初期化の経路の状態でワーカノードを初期化する完全な再生方法よりも効率的であることがわかる。しかし、係る結論は、全てのステップが等しいコストを有することを前提としている。図4を参照して、ワーカノード106又はスケジューラノード104は、後方向のトラッキングステップの数、前方向のトラッキングステップの数を決定し、それらを、分散コンピューティングシステム100のソフトウェアの記号的実行を評価することで決定されるコストと結合することで、初期コストを定量化する。コストは、スケジューラノード104又は他の適切なエンティティにより決定される。コストは、分散コンピューティングシステム100及び検査下にあるプログラムにより使用される特定の記号的実行のエンジンの関数である。また、幾つかのプレディケートが非常に複雑であるとき、コストは、あるステップから別のステップに変化する。次の記号のプレディケートに記号の経路に沿って前方向に計算する平均コストを表す、平均の前方向の計算コストcfが決定されるか又は発見される。前の記号のプレディケートに現在の記号の経路に沿って計算を引き返す取り消す平均のコストを表す平均のバックトラックの計算コストcbが決定されるか又は発見される。係るコストは、バックトラッキング及びリプレイステップの時間の要件を記録するワーカノード106、及び、ワーカノード106から係る情報を収集し、情報を平均し、或いは、引き返し又は再生される必要がある実際のプレディケートについてワーカノード106に記憶されるコスト情報を使用したスケジューラノード104により発見される。1実施の形態では、前方向及び後方向の計算コストは、互いに関して設定される。従って、所与のジョブの完全な再生のオプションの初期化コストは、IPCにおけるステップの数に、前方向のプレディケートステップのコストを乗じたものとして記載される。所与のワーカノード106の引き返し及び再生の初期化コストは、引き返しのプレディケートのステップの数と引き返しのプレディケートのステップのコストとの積に、前方向のプレディケートのステップの数と前方向のプレディケートのステップのコストとの積を加えた合計として記載される。スケジューラノード104は、IPCの完全な再生のコストと、IPCに整合するためにワーカノード106のTPCの引き返し及び再生のコストとの間の最少値を決定することで、あるジョブが割り当てられているワーカノード106の初期化コストを決定する。従って、初期化コストは、ジョブと、ジョブが割り当てられたリソースとの関数である。図9は、分散コンピューティング環境におけるソフトウェアの解析の問題の効率的な並列化のためのノードの計算の初期化技法の方法900の例示的な実施の形態である。1実施の形態では、本方法900は、スケジュールノード104又はワーカノード106により実現される。ステップ905で、あるリソースに割り当てられるべきジョブが選択される。ジョブは、このジョブに関連されるIPCを有する。ジョブを選択する適切な方法が使用される場合がある。ステップ910で、ジョブを割り当てる候補となるリソースが選択される。候補となるリソースを選択する適切な方法が使用される場合がある。ステップ915で、ジョブのIPCにおけるプレディケートの数が決定される。ステップ920で、完全な再生の初期化のコストが決定される。完全な再生の初期化のコストは、IPCにおけるステップ数に前方向ステップのコストを乗じることで発見される。1実施の形態では、前方向ステップのコストは、グローバルに決定される。別の実施の形態では、前方向ステップのコストは、前方向ステップを実行するのに要する時間を評価することで決定される。ステップ925で、IPCと候補となるリソースのTPCとの間の共通のプレフィックスが決定される。共通のプレフィックスは、第一のプレディケートのエレメントで始まる、IPCとTPCとの間で共通する最も長いプレディケートのエレメントのシーケンスである。ステップ930で、共通のプレフィックスに到達するまで、引き返すべきTPCのプレディケートのステップの数が決定される。ステップ935で、引き返しのコストが決定される。引き返しのコストは、ステップ935からの引き返すステップの数に、引き返すステップのコストを乗じることで発見される。1実施の形態では、引き返すステップのコストは、グローバルに決定される。別の実施の形態では、引き返すステップのコストは、引き返すステップを実行するのに要する時間を評価することで決定される。ステップ940で、IPCが完了するまでの、再生されるべき共通のプレフィックス後のIPCからのステップの数が決定される。ステップ945で、再生コストが決定される。再生コストは、IPCを完了するために要する前方向ステップの数に、再生ステップのコストを乗じることで発見される。再生ステップのコストは、引く返しステップのコストと同様にして決定される。ステップ950で、再生及び引き返しのコストは、再生のコストに引き返しのコストを加えたものである。ステップ955で、初期化の再生及び引き返しの方法と初期化の完全な再生の方法とは、どちらが安価であるかを判定するために比較される。よりコストが安い初期化手法が選択される。図4を参照して、スケジューラノード104は、分散コンピューティング環境におけるソフトウェアの解析の問題の効率的な並列化のためのスケジューリングのポリシーを適用する。スケジューラノード104により使用されるスケジューリングのポリシーは、ジョブをワーカノード106に効率的且つ知的に割り当てる適切なスケジューリングのポリシーを含む。スケジューリングのポリシーは、ジョブのキュー210からジョブをどのように選択すべきかに関するポリシーを含む。ジョブのキュー210からジョブを選択する適切なポリシーが選択される。1実施の形態では、ジョブのキュー210は、ファーストイン、ファーストアウトのキューとして構成される。ジョブのキュー210で最初の未解決のジョブが処理され、このジョブは、このキューにおいて最も古いジョブを表す。別の実施の形態では、ジョブのキュー210は、優先度のキューとして実現される。係るケースでは、あるジョブには、サーチポリシーにおける要素のような要素に関する優先度が割り当てられる。例は、深さであり、低い深さでの調査されていない分岐には高い優先度が割り当てられる。これは、グラフの根に近い分岐の下で、かなりのサーチツリーが展開される大きな可能性があるからである。適切な方法は、係るキュー内のジョブの優先度を計算するために使用される。たとえば、ジョブの作成からの記憶されたパラメータは、緊急度を計算するために使用される。係る実施の形態では、スケジューラ104は、最も高い計算された優先度をもつジョブを選択する。スケジューリングポリシーは、利用可能なリソースのリスト212からワーカノード106をどのように選択すべきかに関するポリシーを含む。利用可能なリソースのリスト212は、エントリがリストに追加されたときに対応するタイムスタンプにより順序付けされるリストとして構成される。利用可能なリソースのリスト212からリソースを選択する適切な方法が使用される場合がある。方法のタイプは、利用可能なリソースのリスト212におけるリソースの機能natureに依存する。係るリソースは、計算能力、メモリ、最後の計算状態等の観点で互いに関して同じ種類又は異なる種類である場合がある。リソースの大部分が同じ種類である場合、簡単なリソースの選択が使用され、利用可能なリソースのリスト212に追加される第一のリソースは、割り当てのために選択される。リソースの大部分が異なる場合、より洗練されたリソースの選択が使用され、あるジョブとあるリソースとの間の最も適合したものが決定される。係るケースでは、あるリソースとあるジョブと整合させる基準は、たとえば利用可能な計算能力に比較されるジョブの知覚されるサイズ、利用可能なメモリに比較されるジョブの知覚されるサイズ、又は初期化のコストを含む。1実施の形態では、最も大きな利用可能な計算能力又はメモリを持つリソースが選択される。別の実施の形態では、スケジューラノード104は、利用可能なリソースのリストにおけるどのリソースが、ジョブの初期化の経路の状態と最も長い共通のプレフィックスを共有する終了の経路の状態を有するかを判定することで、初期化のコストに関してジョブに最も適合するリソースを決定する。更に別の実施の形態では、利用可能なリソースのリストにおいてどのリソースが最も長く待機しているかに基づいてリソースが決定される。係る待ち時間の判定は、リソースのタイムスタンプに基づいている。スケジューラノード104は、適切な時間でジョブのキュー210と利用可能なリソースのリスト212とからエントリをスケジュールする。1実施の形態では、スケジュールノード104は、ジョブのキュー210と利用可能なリソースのリスト212とから周期的にエントリをスケジュールする。別の実施の形態では、スケジューラノード104は、何れかの構成への追加が存在するたびに、ジョブのキュー210と利用可能なリソースのリスト212とからエントリをスケジュールする。図10は、分散コンピューティング環境におけるソフトウェアの解析の問題に関する効率的な並列化のためのスケジューリングポリシーを実現する方法1000の例示的な実施の形態である。1実施の形態では、本方法1000は、スケジュールノード104により実現される。ステップ1005で、あるジョブが選択される。ジョブは、ジョブのキューから選択される。1実施の形態では、ジョブは、ファーストイン、ファーストアウトに従って選択される。別の実施の形態では、ジョブは、最も高い優先度が割り当てられるジョブを決定することで選択される。ステップ1007で、あるリソースが利用可能なリソースのリストから選択される。1実施の形態では、そのジョブに最も適合するリソースは、利用可能なリソースのリストにおいて待機しているリストのなかから発見される。別の実施の形態では、リソースは、ファーストイン、ファーストアウトに基づいて選択される。最も適合するリソースの基準は、所与のリソースに関するジョブの初期化のコスト、或いは、所与のリソースで利用可能な計算能力又はメモリの量を含む。ステップ1007は、ステップ1010~1020で実現される。ステップ1010で、それぞれのリソースの前のジョブで実行された最後の状態を考慮して、利用可能なリソースのリストにおけるそれぞれのリソースについて、ジョブの初期化のコストが計算される。初期化のコストの計算の適切な方法が使用される場合がある。係る実行された最後の状態は、リソースに記憶されたとき、ジョブに依存して、初期化のコストを少なくする。ステップ1015で、リストにおけるどのリソースが、抽出されたジョブについて最も低い初期化のコストを有するかが判定される。最も適合するリソースを決定するために別の基準が使用される場合、推論の判定corollarydeterminationが行われる。ステップ1020で、最も適合されたリソースが選択される。1を超えるリソースが最も適合するリソースとなる場合、最も古いタイムスタンプをもつリソースが選択される。ステップ1025で、選択されたリソースでの記号的実行についてジョブがスケジュールされる。ステップ1030で、未解決のジョブを表すジョブのキュー、又はジョブが割り当てられるべきワーカノードを表す利用可能なリソースのリストの何れかが空であるかが判定される。何れかが空である場合、スケジューリングが行われず、本方法は、別の係るリソースが到来するまで終了される。しかし、両方のジョブが未解決であって、リソースが待機している場合、本方法1000は、何れかの係るキューが空となるまで繰り返される。図5~7,9~10は、例示的な方法500,600,700,900及び1000に関して行われるべき特定のステップの数を開示しているが、本方法500,600,700,900及び1000は、図5~7,9~10で示されるステップよりも多いステップ又は少ないステップで実行される。さらに、図5~7,9~10は、方法500,600,700,900及び1000に関して行われるべきステップの所定の順序を開示しているが、本方法500,600,700,900及び1000を含むステップは、適切な順序で行われる。図5~7,9~10の幾つかの部分は、図5~7,9~10の他の1以上の文脈で上手く実行される場合がある。本方法500,600,700,900及び1000は、図1~6及び8のシステム、方法500,600,700,900及び1000を実現するために動作する他のシステム、ネットワーク又はデバイスを使用して実現される。所定の実施の形態では、本方法500,600,700,900及び1000は、コンピュータ読み取り可能な記録媒体で実行されるソフトウェアで部分的又は完全に実現される。この開示のため、コンピュータ読み取り可能な記録媒体は、ある期間についてデータ及び/又は命令を保持する手段又は手段の集合を含む。コンピュータ読み取り可能な記録媒体は、限定されるものではないが、ダイレクトアクセスストレージデバイスたとえばハードディスクドライブ又はフロプティカルディスク、シーケンシャルアクセスストレージデバイスたとえばテープディスクドライブ、コンパクトディスク、CDROM、DVD、ランダムアクセスメモリRAM、リードオンリメモリROM、電子的に消去可能なプログラム可能なリードオンリメモリEEPROM、及び/又はフラッシュメモリ、並びに、配線、光ファイバのような伝送媒体、他の有形の一時的でない媒体、及び/又は上述したものの組み合わせを含む。本実施の形態の開示が詳細に記載されたが、この開示の精神及び範囲から逸脱することなしに様々な変形、置き換え及び変更を行うことができる。以下、本発明の特徴点を付記として示す。付記1ソフトウェアを検証する方法であって、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定するステップと、前記初期化の経路の状態は、検証されるべきソフトウェアの開始の状態に到達するためのプログラムのプレディケートのシーケンスを含み、前記受信されたソフトウェアの検証のジョブは、検証されるべきソフトウェアの一部の指示を含み、計算ノードの終了の経路の状態を決定するステップと、前記終了の経路の状態は、前記計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達される最後の状態の指示を含み、前記計算ノードは、前記受信されたソフトウェアの検証のジョブを実行するために割り当てられ、前記初期化の経路の状態と前記終了の経路の状態とに基づいて計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップと、を含むことを特徴とする方法。付記2前記ソフトウェアを検証することは、コードに記号的実行を施すことを含む、付記1記載の方法。付記3引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するステップを更に含み、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含む、を含む付記1記載の方法。付記4引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含み、再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップと、前記再生手法は、前記初期化の経路の状態のプレディケートステップを再生することを含み、前記計算されたコストのうちの低い方のコストをもつ初期化の手法を選択するステップと、を更に含む付記1記載の方法。付記5前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、平均の前方向の計算コストを使用することを含み、前記平均の前方向の計算コストは、前記ソフトウェアの検証の間に次のプレディケートに検証の経路に沿って前方向に計算する平均のコストを含む、付記4記載の方法。付記6前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、平均の引き返しの計算コストを使用することを含み、前記平均の引き返しの計算コストは、前記ソフトウェアの検証の間に前のプレディケートに検証の経路に沿って引き返す平均のコストを含む、付記4記載の方法。付記7前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算するステップは、所与の手法により前記受信されたソフトウェアの検証のジョブの実行を初期化するために必要とされる前方向のステップと引き返しのステップとを使用することを含む、付記4記載の方法。付記8コンピュータ読み取り可能な記録媒体と、前記コンピュータ読み取り可能な記録媒体に担持されるコンピュータ実行可能な命令とを備える製品であって、前記コンピュータ実行可能な命令は、プロセッサにより読取り可能であり、前記コンピュータ実行可能な命令は、読み取られて実行されたときに、前記プロセッサに、受信されたソフトウェアの検証のジョブの初期化の経路の状態を決定させ、前記初期化の経路の状態は、検証されるべきソフトウェアの開始の状態に到達するためのプログラムのプレディケートのシーケンスを含み、前記受信されたソフトウェアの検証のジョブは、検証されるべきソフトウェアの一部の指示を含み、計算ノードの終了の経路の状態を決定させ、前記終了の経路の状態は、前記計算ノードでの前のソフトウェアの検証のジョブの実行の間に到達される最後の状態の指示を含み、前記計算ノードは、前記受信されたソフトウェアの検証のジョブを実行するために割り当てられ、前記初期化の経路の状態と前記終了の経路の状態とに基づいて計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化させる、ことを特徴とする製品。付記9前記ソフトウェアを検証することは、コードに記号的実行を施すことを含む、付記8記載の製品。付記10前記コンピュータ実行可能な命令は、前記プロセッサに、更に、引き返し及び再生手法を使用して、前記計算ノードでの前記受信されたソフトウェアの検証のジョブの実行を初期化させ、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含む、を含む付記8記載の製品。付記11前記コンピュータ実行可能な命令は、前記プロセッサに、更に、引き返し及び再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算させ、前記引き返し及び再生手法は、前記終了の経路の状態から開始して、経路の状態が前記初期化の経路の状態のプレフィックスと同じになるまで、前記終了の経路の状態に到達するために要するプレディケートステップを引き返すこと、及び前記プレフィックスで開始して、前記初期化の経路の状態に到達するまで、前記初期化の経路の状態の残りのプレディケートステップを再生することを含み、再生手法を使用して、前記受信されたソフトウェアの検証のジョブの実行を初期化するコストを計算させ、前記再生手法は、前記初期化の経路の状態のプレディケートステップを再生することを含み、前記計算されたコストのうちの低い方のコストをもつ初期化の手法を選択させる、付記8記載の製品。付記12前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、平均の前方向の計算コストを使用することを含み、前記平均の前方向の計算コストは、前記ソフトウェアの検証の間に次のプレディケートに検証の経路に沿って前方向に計算する平均のコストを含む、付記11記載の製品。付記13前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、平均の引き返しの計算コストを使用することを含み、前記平均の引き返しの計算コストは、前記ソフトウェアの検証の間に前のプレディケートに検証の経路に沿って引き返す平均のコストを含む、付記11記載の製品。付記14前記受信されたソフトウェアの検証のジョブの実行を初期化するコストの計算は、所与の手法により前記受信されたソフトウェアの検証のジョブの実行を初期化するために必要とされる前方向のステップ数と引き返しのステップ数とを使用することを含む、付記11記載の製品。"