一つまたは複数のコンピューティングデバイスによって:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを含む、方法。請求項1記載の方法であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、方法。請求項1または2記載の方法であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、方法。請求項3記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、方法。請求項1ないし4のうちいずれか一項記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが:前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、方法。請求項1ないし5のうちいずれか一項記載の方法であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、方法。請求項6記載の方法であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、方法。請求項7記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。請求項7記載の方法であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。一つまたは複数のプロセッサによって実行可能な命令を有するメモリと;前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作する、システム。ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティングデバイスによって実行されたときに:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作可能である、媒体。請求項11記載の媒体であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、媒体。請求項11または12記載の媒体であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、媒体。請求項13記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、媒体。請求項11ないし14のうちいずれか一項記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが:前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、媒体。請求項11ないし15のうちいずれか一項記載の媒体であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、媒体。請求項16記載の媒体であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、媒体。請求項17記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。請求項17記載の媒体であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、手段と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する手段と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する手段と;前記第一および第二の数値制約条件のそれぞれを式で表現する手段と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う手段とを含む、システム。本発明は、従来技術の欠点を軽減または解消する。本発明の課題は、請求項記載の手段によって達成される。本開示について、これから付属の図面に示されるような若干の実施形態を参照しつつ詳細に述べる。以下の記述において、本開示の十全な理解を与えるために数多くの具体的詳細が記載されるが、当業者には、本開示がそのような具体的詳細の一部または全部がなくても実施されうることは明白であろう。その一方、よく知られた処理ステップおよび/または構造は、本開示を無用に埋没させないよう、詳細に述べてはいない。さらに、本開示は具体的実施形態との関連で記述されるが、この記述は本開示を記述される実施形態に限定することを意図したものではないことは理解しておくべきである。逆に、この記述は付属の請求項によって定義される本開示の精神および範囲内に含まれうる代替、修正および等価物をカバーすることが意図されている。ソフトウェアアプリケーションはしばしばいくつかのソフトウェアモジュールに編成され、各ソフトウェアモジュールは具体的な機能を実行するコードを含みうる。典型的な筋書きでは、ソフトウェアモジュールは入力または出力変数をいくつ有していてもよい。ソフトウェアモジュールが呼び出されるとき、ソフトウェアモジュールの入力変数に割り当てられる値として、実際の入力値がたとえばソフトウェアモジュールを呼び出すコードによってソフトウェアモジュールに渡されてもよい。ソフトウェアモジュールのコードは、実際の入力値との関連で実行されうる。最終的には、ソフトウェアモジュールの出力変数についての実際の出力値が決定され、ソフトウェアモジュールによって返されることができ、その時点でソフトウェアモジュールはその実行を完了する。さらに、ソフトウェアモジュールのコードによって決定される実際の出力値は、通例、ソフトウェアモジュールにその呼び出しの際に渡される実際の入力値に依存する。さらに、ソフトウェアモジュールは、中間変数とも称されるローカル変数をいくつ有していてもよい。ローカル変数の値も直接または間接的に、入力変数の値に依存しうる。ローカル変数はローカルなスコープをもつ。ローカル変数は、そのローカル変数が宣言されているソフトウェアモジュールのコンテキスト内でのみ存在し、該コンテキスト内からのみアクセス可能である。これに対し、ソフトウェアモジュールが属するソフトウェアアプリケーションは、グローバル変数をいくつ有していてもよい。グローバル変数は、ソフトウェアアプリケーション自身の中においてグローバルなスコープをもち、ソフトウェアアプリケーションに属すすべてのソフトウェアモジュールにとってアクセス可能である。ソフトウェアモジュールが呼び出されるとき、ソフトウェアモジュールはグローバル変数の値にアクセスするまたはグローバル変数の値を修正してもよく、値修正はソフトウェアモジュールがその実行を完了した後でさえ持続する。具体的実施形態では、第一の変数の値が第二の変数の値に基づいて決定されるすなわち、第一の変数の値が第二の変数の値に依存するとき、第一の変数は第二の変数に依存すると考えられる。変数は、入力変数であれ出力変数であれ、またローカル変数であれグローバル変数であれ、通例、特定のデータ型をもつ。データ型はたとえば、限定するものではないが、キャラクタまたは文字、ストリングまたは文字列、整数、浮動小数点、倍精度、ブーリアン、ポインタ、配列および列挙といったものである。変数のデータ型は、どのような型のデータたとえば実際の値がその変数に割り当てられてもよいかを示す。たとえば、整数型の変数には整数値だけが割り当てられるべきであり、ブーリアン型の変数には真偽値だけが割り当てられるべきである。異なるプログラミング言語は、特定の言語で書かれたソフトウェアモジュールまたはアプリケーションの変数がもちうる異なるデータ型や、それらの特定のデータ型に適用されうる異なる演算を定義することがある。具体的実施形態では、プログラミング言語のデータ型は二つの範疇に分けられる:ストリングと数値である。数値データ型は、たとえば限定するものではないが整数、浮動小数点、倍精度およびブーリアンといった非ストリングデータ型を含んでいてもよい。ストリングは多くのプログラミング言語において利用可能なデータ型である。ただ、異なるプログラミング言語はストリングを異なる仕方で定義することもある。たとえば、ジャバJavaプログラミング言語は型stringをジャバクラスjavalangStringとして定義する。これは、ストリングをキャラクタのイミュータブルなアレイとして表す。この場合、ひとたびストリング変数が宣言され、生成されると、その値はその後変えることができない。ストリング変数の値へのいかなる修正も、新しいストリング変数が宣言され、構築されることにつながる。クラスjavalangStringはメソッドと称される、ストリング変数に適用されうる多くの演算をも提供する。他方、Cプログラミング言語では、ストリングは、ヌルキャラクタで終わる一次元キャラクタ配列として定義されうる。Cのストリングはミュータブルであり、その値はその場で修正されうる。実は、配列内の各キャラクタは個別に修正されてもよい。各プログラミング言語は一般にいくつかの数値データ型を定義する。ただ、利用可能な具体的な数値データ型は言語によって異なることがある。整数、浮動小数点、倍精度およびブーリアンはたいていのプログラミング言語によって一般的に定義される数値データ型である。ここでもまた、異なるプログラミング言語は具体的な数値データ型を異なる仕方で定義することもある。たとえば、ジャバプログラミング言語は整数変数を宣言する二つの方法を提供する:プリミティブデータ型intとして、あるいはジャバクラスjavalangIntegerとしてである。クラスjavalangIntegerは整数変数に適用されうる演算すなわちメソッドを提供する。他方、Cは、異なるデータサイズをもつ整数変数を宣言するために使用されうる三つのプリミティブデータ型shortintlongを提供する。時に、ソフトウェアモジュールの入力、出力またはローカル変数に対して課される制約条件がいくつかあることがある。具体的実施形態では、変数に課される制約条件は、たとえば、限定するものではないが、その変数にどんな値が割り当てられてもよいか、その変数に割り当てられてもよいデータ値のサイズ、あるいはその変数に対して課される他の任意の適用可能な条件もしくは制限を指定してもよい。そのような変数制約条件は、ソフトウェアモジュールの設計仕様もしくは形式上の要求、そのソフトウェアモジュールを実装するために使われるプログラミング言語の仕様、そのソフトウェアモジュールのプログラミング論理に含まれるコード、そのソフトウェアモジュールが実行される実行時環境または他の適用可能な因子によって、またはそれらの因子から、指定されてもよい。たとえば、整数変数aに課されうる制約条件は、ソフトウェアモジュールが4バイトを使って各整数を表す実行時環境内で実行されるため、整数変数aが0xFFFFFFFF以下の割り当てられた整数値であることしかできないことを指定する。この場合、整数変数aに課された制約条件は、式a<0xFFFFFFFFとして表現されてもよい。もう一つの例として、ストリング変数sに対して課されうる制約条件は、ストリング変数sの長さすなわちキャラクタ数が8でなければならないことを指定する。この場合、ストリング変数sに対して課される制約条件は、別の式slength=8として表現されてもよい。時に、ソフトウェアモジュールの一つの変数に対して課される制約条件は、直接または間接に、ソフトウェアモジュールの別の変数の値に課される制約条件に依存してもよい。たとえば、整数変数bに対して共同して課されうる二つの制約条件は:1整数変数bは-10以上の割り当てられた整数値であることしかできない、2整数変数bは変数aの値より小さな割り当てられた整数値であることしかできないことを指定する。この場合、組み合わせて整数変数bに課される二つの制約条件は、各制約条件を別個の式として表して、と表現されてもよい。具体的実施形態では、ソフトウェアモジュールは数値またはストリング変数をいくつ有していてもよく、これらの変数はソフトウェアモジュールの入力変数であっても、あるいはローカルすなわち中間変数であってもよい。具体的実施形態では、一組の制約条件がソフトウェアモジュールの特定の数値またはストリング変数に対して課されてもよい。一組の制約条件がソフトウェアモジュールの一つ一つすべての変数に課されることは必要ではないことを注意しておく。具体的実施形態では、数値変数が与えられたとき、該数値変数は、数値制約条件またはストリング制約条件をいくつ有していてもよい。たとえば、整数変数bは、その値が-10以上でなければならないことを指定する数値制約条件たとえば、制約条件b-10を有していてもよい。整数変数bはまた、その値のテキストすなわちストリング表現がストリング182に等しくなければならないことを指定するストリング制約条件たとえば、制約条件btoString182を有していてもよい。この場合、整数変数bに課される制約条件の集合は、数値制約条件とストリング制約条件の両方を含み、したがって、ハイブリッドの制約条件の集合であるたとえば、182。同様に、具体的実施形態において、ストリング変数を与えられたとき、該ストリング変数は、ストリング制約条件または数値制約条件をいくつ有していてもよい。たとえば、ストリング変数sは、その値が部分ストリングcaで始まらなければならないことを指定するストリング制約条件たとえば、制約条件ssubstringcaまたはsstartsWithを有していてもよい。ストリング変数sはまた、その値が8キャラクタの長さをもたなければならないことを指定する数値制約条件たとえば、制約条件slength8を有していてもよい。この場合もまた、ストリング変数sに課される制約条件の集合は、数値制約条件およびストリング制約条件の両方を含み、したがってハイブリッドの制約条件の集合であるca8。具体的実施形態では、ソフトウェアモジュールに課される制約条件は、入力変数、出力変数およびローカル変数を含むその変数に対して課される制約条件すべてを組み合わせて含んでいてもよい。たとえば、整数変数bおよびストリング変数sが両方ともソフトウェアモジュールmに属するとする。この場合、ソフトウェアモジュールm自身に課される制約条件の集合は、変数bおよびsにそれぞれ課される制約条件の二つの集合の論理和を含み、これは182ca8に等しい。この集合は数値制約条件およびストリング制約条件の両方を含むので、これもハイブリッドの制約条件の集合である。具体的実施形態では、任意の数の数値変数またはストリング変数を有するソフトウェアモジュールに課されるハイブリッドの制約条件の集合を決定および解決することが有用であることがありうる。ソフトウェアモジュールの特定の変数に対して課されるハイブリッドの制約条件の集合を決定および解決することも有用であることがありうる。具体的実施形態では、制約条件の集合を解決するsolvingとは、集合に含まれる制約条件すべてを満たす一つまたは複数の解を見出すことを試みることを意味する。図1は、ソフトウェアモジュールまたはソフトウェアモジュールの変数に対して課される制約条件を決定および解決するための例示的方法を示している。図2は、ソフトウェアモジュールまたはソフトウェアモジュールの変数に対して課される制約条件を決定および解決するためのシステム200を示している。具体的な実施形態では、図2に示されるシステム200のコンポーネントは、コンピュータハードウェアもしくはソフトウェアまたはそれらの組み合わせとして実装されてもよい。図1および図2については、互いとの関連で記述する。具体的実施形態では、ソフトウェアモジュールは任意の数の数値変数またはストリング変数を有していてもよい。たとえば、ソフトウェアモジュールmは整数変数vi、ブーリアン変数vbおよびストリング変数vsを有していてもよい。この場合、変数viおよびvbは数値変数である。具体的実施形態では、これらの変数はソフトウェアモジュールの入力変数、出力変数またはローカル変数であってもよい。具体的実施形態では、最初に、ソフトウェアモジュールの特定の諸数値変数に対して課される任意の数の数値制約条件およびソフトウェアモジュールの特定の諸ストリング変数に対して課される任意の数のストリング制約条件があってもよい。より具体的には、ある特定の数値変数に対して一組の数値制約条件が指定され、課されてもよく、あるいはある特定のストリング変数に対して一組のストリング制約条件が指定され、課されてもよい。制約条件の各組は、一つまたは複数の個別的な制約条件を含んでいてもよい。たとえば、整数変数viに対して数値制約条件numericconstraintの集合nc1viが指定され、課されてもよく、ブーリアン変数vbに対して数値制約条件の集合nc1vbが指定され、課されてもよく、ストリング変数vsに対してストリング制約条件stringconstraintの集合sc1vsが指定され、課されてもよい。具体的実施形態では、これらの制約条件の初期集合たとえば、nc1vinc1vbおよびsc1vsは、ソフトウェアモジュールの設計仕様または形式的な要求に基づいて指定されてもよい。具体的実施形態では、ソフトウェアモジュール内で、ソフトウェアモジュールの個別的な諸数値変数に適用される、数値入力を受けるまたは数値出力を生成する演算がいくつあってもよい。たとえば、整数変数viに適用される演算はrivi10であってもよい。これは、viの値および10の二つの数値を入力として受け、数値つまりriの値を出力として生成する。具体的実施形態では、ソフトウェアモジュール内で、ソフトウェアモジュールの個別的な諸数値変数に適用される、ストリング入力を受けるまたはストリング出力を生成する演算がいくつあってもよい。たとえば、ブーリアン変数vbに適用される演算はvbtoStringであってもよい。これは、ブーリアン変数vbの値のストリング表現であるストリング値を出力として生成する。具体的実施形態では、ソフトウェアモジュール内で、ソフトウェアモジュールの個別的な諸ストリング変数に適用される、ストリング入力を受けるまたはストリング出力を生成する演算がいくつあってもよい。たとえば、ストリング変数vsに適用される演算はrsvsconcatであってもよい。これは、vsの値およびabcの二つのストリング値を入力として受け、ストリング値、つまりrsの値を出力として生成する。具体的実施形態では、ソフトウェアモジュール内で、ソフトウェアモジュールの個別的な諸ストリング変数に適用される、数値入力を受けるまたは数値出力を生成する演算がいくつあってもよい。たとえば、ストリング変数vsに適用される演算はvslengthであってもよい。これは、ストリング変数vsの値に含まれるキャラクタの数を示す数値をその出力として生成する。ストリング変数vsに適用されるもう一つの演算は、二つの数値を入力として取るvssubstringであってもよい。具体的実施形態は、図1のステップ102に示されるように、ソフトウェアモジュールたとえばソフトウェアモジュールmと、ソフトウェアモジュールの個別的な数値変数に対して最初に指定され、課されている数値制約条件の集合たとえば、整数変数viに課される数値制約条件nc1viおよびブーリアン変数vbに課される数値制約条件nc1vbと、ソフトウェアモジュールの個別的なストリング変数に対して最初に指定され、課されているストリング制約条件の集合たとえば、ストリング変数vsに課されるストリング制約条件sc1vsとを解析してもよい。具体的実施形態では、数値制約条件およびストリング制約条件は、最初、ソフトウェアモジュールの入力変数または中間変数すなわちローカル変数に課されていてもよい。もちろん、具体的実施形態では、ソフトウェアモジュールの一つ一つすべての数値変数に数値制約条件の集合が最初に課されており、ソフトウェアモジュールの一つ一つすべてのストリング変数にストリング制約条件の集合が最初に課されていることは必要ではない。特定の諸数値変数だけが関連付けられた数値制約条件を最初に有している、あるいは特定の諸ストリング変数だけが関連付けられたストリング制約条件を最初に有していることも可能である。具体的実施形態では、ソフトウェアモジュールの入力変数に最初に課されていた数値制約条件またはストリング制約条件について、該制約条件は、ソフトウェアモジュールの設計仕様または形式的な要求に従って決定されてもよい。ソフトウェアモジュールの中間変数に最初に課されていた数値制約条件またはストリング制約条件について、該制約条件は、ソフトウェアモジュール上で記号的実行を行うことによって決定されてもよい。記号的実行symbolicexecutionは、下記で図8との関連でより詳細に述べる。手短に言うと、具体的実施形態は、ソフトウェアモジュールの各入力変数に記号的値symbolicvalueを代入しながらソフトウェアモジュール上で記号的実行を行ってもよい。ソフトウェアモジュールの中間変数は、直接または間接に、ソフトウェアモジュールの入力変数のうちの一つまたは複数の入力変数に依存することがあるので、ソフトウェアモジュール上で記号的実行を行う結果として、該中間変数について、それが前記特定の入力変数に対してもつ依存性を示す記号的表現symbolicexpressionの集合が与えられうる。具体的実施形態は次いで、該中間変数について得られた記号的表現の前記集合と、該中間変数が依存する前記特定の入力変数に課される前記制約条件に基づいて、該中間変数に課される制約条件の集合を決定しうる。たとえば、ソフトウェアモジュールmに関し、viが入力変数、riが中間変数であり、rivi10であるとする。この場合、ソフトウェアモジュールm上で記号的実行を行うことで、中間変数riが入力変数viに依存することを決定しうる。さらに、入力変数viに対して、vi0というような数値制約条件が課されているとする。記号的実行の結果および入力変数viに課される数値制約条件に基づいて、中間変数riについて、ri10のような数値制約条件が決定されうる。図1のステップ102に示される解析から、図1のステップ104に示されるように、具体的実施形態は、ソフトウェアモジュールの個別的な数値変数に課されるストリング制約条件の集合と、ソフトウェアモジュールの個別的なストリング変数に課される数値制約条件の集合を推定しうる。具体的実施形態では、図1のステップ102および104は、図2に示されるシステム200のコンポーネント202相互的制約条件発生器/クロス制約条件発生器によって実行されてもよい。具体的実施形態では、コンポーネント202はソフトウェアモジュール212およびソフトウェアモジュール212の変数に最初に課される制約条件214を入力として取りうる。制約条件214はソフトウェアモジュールの数値変数に対して最初に指定され、課される数値制約条件およびソフトウェアモジュールのストリング変数に対して最初に指定され、課されるストリング制約条件を含んでいてもよい。コンポーネント202は、ソフトウェアモジュール212の数値変数に課されることになるストリング制約条件およびソフトウェアモジュール212のストリング変数に課されることになる数値制約条件を推定するために適用可能な解析を実行してもよい。コンポーネント202は、ソフトウェアモジュール212の変数に課される指定された制約条件および推定された制約条件の両方を含む数値制約条件およびストリング制約条件のハイブリッドの集合を出力として提供しうる。具体的実施形態では、ソフトウェアモジュールの変数についての制約条件は、さまざまな因子に基づいて推定されてもよく、本開示は任意の適用可能な因子を考えている。たとえば、限定するものではないが、特定の変数に適用される演算、ソフトウェアモジュールを実装するために使われるプログラミング言語の仕様、ソフトウェアモジュールが実行される実行時環境または複数の因子の組み合わせに基づいて、数値制約条件が数値変数およびストリング変数の両方について推定されてもよく、ストリング制約条件が数値変数およびストリング変数の両方について推定されてもよい。具体的実施形態では、数値変数を与えられたとき、該数値変数に適用される、ストリング結果を生じうる演算に基づいてストリング制約条件が推定されてもよい。たとえば、ソフトウェアモジュールmにおいて整数変数viに次の二つの演算splitが適用されるとする。これは、まず整数変数viの値のストリング表現たとえば数182がストリング182として表現されるを生成し、次いでそのストリングを、キャラクタ0の位置で、二つの新しいストリングに分割する。第二の演算すなわちストリング分割演算が成功するたとえば、結果としてヌルストリングを生じないために、それらの演算から、整数変数viの値のストリング表現が少なくとも一つのキャラクタ0を含まなければならないというストリング制約条件が推定されてもよい。具体的実施形態では、数値変数が与えられたとき、該数値変数に適用される、数値結果を生じうる演算に基づいて数値制約条件が推定されてもよい。たとえば、ソフトウェアモジュールmにおいて整数変数viに次の演算Mathsqrtが適用されるとする。これは、整数変数viの値の平方根を与える。この演算をエラーに遭遇することなく実行するために、この演算から、整数変数viの値が0以上でなければならないという数値制約条件が推定されてもよい。具体的実施形態では、ストリング変数を与えられたとき、該ストリング変数に適用される、ストリング結果を生じうる演算に基づいてストリング制約条件が推定されてもよい。たとえば、ソフトウェアモジュールmにおいてストリング変数sに次の演算sreplaceAllが適用されるとする。これは、ストリング変数sの値において見出されるすべての部分ストリングabcをxyzで置換する。この演算がストリング変数sに対して何らかの実際の効果をもつために、この演算から、ストリング変数sの値が少なくとも一つの部分ストリングabcの生起を含まなければならないというストリング制約条件が推定されてもよい。具体的実施形態では、ストリング変数を与えられたとき、該ストリング変数に適用される、数値結果を生じうる演算に基づいて、あるいは該ストリング変数に適用される、一つまたは複数の数値入力を取りうる演算に基づいて、数値制約条件が推定されてもよい。たとえば、ソフトウェアモジュールmにおいてストリング変数sに次の演算sstartsWithが適用されるとする。これは、ストリング変数sの値が部分ストリングabcで始まるかどうかを示すブーリアン結果を真または偽として与える。この演算の実行が成功するためには、ストリング変数sの値は少なくとも三つの文字を有する必要がある。よって、この演算から、ストリング変数sの長さが3以上でなければならないという数値制約条件が推定されうる。もう一つの例として、ソフトウェアモジュールmにおいてストリング変数sに数値を入力として取る次の演算ssubstringも適用されるとする。この演算の実行が成功するたとえば結果としてヌルストリングを生じないためには、ストリング変数sの値は少なくとも6文字を有する必要がある。よって、この演算から、ストリング変数sの長さが6以上でなければならないという数値制約条件が推定されうる。上記の例において、ソフトウェアモジュール内において、ストリング結果を生じる演算が数値変数に適用されることがあり、あるいは数値入力を取るか数値結果を生じる演算がストリング変数に適用されることがある。具体的実施形態では、これらの演算から、個別的なストリング変数に対して数値制約条件が推定され、課されることができ、個別的な数値変数に対してストリング制約条件が推定され、課されることができる。具体的実施形態では、数値変数であれストリング変数であれ変数が与えられたとき、該変数に課される制約条件の完全な集合は、該変数についてもしあれば最初に指定された制約条件と、該変数についてもしあれば推定された制約条件の両方を含む。この制約条件の集合は、数値制約条件またはストリング制約条件または両方を含むことがありうる。変数に対して課される制約条件の集合が、該変数に適用される個々の演算に基づいて該変数について推定された制約条件を含むことがあるので、具体的実施形態はこのようにして得られた制約条件の集合のことを、制約条件の相互作用するハイブリッドな集合interactinghybridsetofconstraintsと称する。具体的実施形態では、任意の数の数値変数またはストリング変数を有するソフトウェアモジュールが与えられたとき、ソフトウェアモジュール自身に課される制約条件の集合は、該ソフトウェアモジュールの個々の変数に課される制約条件すべてを含む。ソフトウェアモジュールの変数またはソフトウェアモジュール自身に課される制約条件のハイブリッドの集合を与えられたとき、図1のステップ106に示されるように、具体的実施形態は、前記集合中の各数値制約条件を数式で表現してもよくたとえば、vi0、vbtrueまたはslength6、前記集合中の各ストリング制約条件を有限状態機械FSMfinitestatemachineで表現してもよい。一般に、FSMは有限個の状態、該状態間の遷移および作用からなる挙動のモデルである。具体的実施形態では、FSMはストリングを表現するために使用されてもよい。図3は、ストリングを表現するために使われるいくつかのFSMを示している。図3では、各FSMについて、中間状態intermediatestateは一本線の丸で表され、受け容れ状態acceptingstateは二本線の丸で表され、状態への入力は丸につながる矢印によって表されている。たとえば、FSM310は、任意のキャラクタを有することができ任意の長さでよいストリングSを表す。FSM320は、少なくとも一つのキャラクタを有し、当該ストリング最後のキャラクタがZであり、制約条件SendsWithtrueを表すために使われてもよいストリングSを表す。FSM330は三つ以上のキャラクタを有し、制約条件Slength3を表すために使われてもよいストリングSを表す。FSM340は、少なくとも一つのキャラクタを有し、少なくとも一つのZを含むストリングSを表す。Z遷移はストリング中の最後のZを表す。FSM350は、Zであるキャラクタを全くもたないストリングSを表す。制約条件を考える。この制約条件から、a0であればZであることが推定できる。FSM340は、上記の制約条件が満足される場合を表している。すなわち、ストリングSは少なくとも一つのZキャラクタを含み、S中に現れる最後のZはaの値に等しいインデックスにある。他方、FSM350は制約条件の前記集合が満足されない場合を表す。つまり、ストリングSはキャラクタZを全く含まず、よってa-1である。これから、制約条件aSlastIndexOfは記号的実行木における岐路forkにつながり、一方の分枝では追加的な数値制約条件a0をもつFSM340の場合を想定し、他方の分枝では追加的な制約条件a-1をもつFSM350の場合を想定する。図4は、ストリングSおよびその部分ストリングの一つSsubstringを表すために使われるもう一つの例示的なFSM400を示す。この例では、状態402がストリングSの開始点であり、状態404がストリングSの受容状態すなわち終点である。部分ストリングSsubstringは、三番目のキャラクタで始まり、五番目のキャラクタで終わるSの部分ストリングである。ジャバプログラミング言語によれば、インデックス付けは0で始まる、つまり最初の要素のインデックス番号が0であることを注意しておく。よって、インデックス番号2は三番目の要素を指し、インデックス番号4は五番目の要素を表すのである。部分ストリングSsubstringについて、開始点はストリングSの開始状態402から進んで三番目の状態であり、これはストリングSの三番目のキャラクタに対応する。図4では、開始状態402から進んで三番目の状態である三つの状態412A、412B、412Cがあり、これらのうちのいずれもが部分ストリングSsubstringについての可能な開始状態412である。部分ストリングSsubstringについて、終点すなわち受容状態はストリングSの開始状態402から進んで五番目の状態であり、これはストリングSの五番目のキャラクタに対応する。図4では、開始状態402から進んで五番目の状態である三つの状態414A、414B、414Cがあり、これらのうちいずれも部分ストリングSsubstringについての可能な受容状態414である。図4において、εはヌル入力遷移を示すことを注意しておく。具体的実施形態では、任意の制約条件の集合が与えられたとき、該集合からの各数値制約条件は適用可能な数式を使って表現されてもよく、該集合からの各ストリング制約条件は適用可能なFSMを使って表現されてもよい。さらに、このように表現された制約条件の集合を与えられたとき、具体的実施形態は、図1のステップ108において示されるように、前記集合中の制約条件すべてを同時に満たす一つまたは複数の解を見出すためにそれらの制約条件を解決することを試みてもよい。具体的実施形態では、図1のステップ108は、図2に示されるシステム200のコンポーネント204によって実行されてもよい。具体的な実施形態では、コンポーネント204は背景理論の枠内での充足可能性SMTSatisfiabilityModuloTheoriesに部分的に基づいて実装される拘束条件ソルバであってもよい。具体的実施形態では、コンポーネント204は、数式を使って表現された数値制約条件およびFSMを使って表現されたストリング制約条件のいずれかまたは両方を含んでいてもよい制約条件の集合を入力として取り、該集合からの制約条件すべてを満たす一つまたは複数の解を見出そうと試みてもよい。何らかの解が見出されうる場合、コンポーネント204はその解を出力として与えてもよい。もちろん、制約条件の集合が、該集合からの制約条件すべてを満たす解を全くもたないこともありうる。たとえば、制約条件の集合0を考える。ここで、sおよびqはストリングであり、aおよびbは整数である。この集合からの制約条件すべてを同時に満たすことのできるsqabについての値の組み合わせは存在しない。したがって、この特定の制約条件の集合は充足不可能である。具体的実施形態は、逐次反復アルゴリズムを使ってハイブリッドの制約条件の集合を解いてもよい。具体的実施形態は、前記集合からの、FSMを使って表現されているストリング制約条件すべてをストリングドメインにおいてグループ化し、前記集合からの、数式を使って表現されている数値制約条件すべてを数値ドメインにおいてグループ化する。具体的実施形態は次いで、数値ドメインまたはストリングドメインいずれか単独における一つまたは複数の解すなわち、前記集合中の数値制約条件すべてまたは前記集合中のストリング制約条件すべてのどちらかを満足する解を見出すことを試み、一方のドメインで見出された解を他方のドメインに供給することを、1前記集合中の数値制約条件およびストリング制約条件のすべてを満足する一つまたは複数の解が見出される;2前記集合中の制約条件すべてを満たす解が存在しないと判定される;あるいは3実行された逐次反復数が所定の閾値に達した、のうちいずれか最初に起こるものが生起するまで、逐次的に行ってもよい。具体的実施形態は、SMTソルバを使って数値領域における数値制約条件を解決し、正規表現の併合、交わり、補集合、クリーネスターKleenestarおよび他の適用可能なアルゴリズムを使ってストリングドメイン中のストリング制約条件を解決してもよい。さらに、具体的実施形態は、制約条件のハイブリッドの集合について一つまたは複数の解を見出すことを試みるときに、次のことを考慮に入れてもよい。第一に、数値ドメイン単独における数値制約条件が充足不可能である場合つまり、前記集合中の数値制約条件だけを満足する解すら存在しない場合、制約条件の集合全体も充足不能である。第二に、ストリングドメイン単独におけるストリング制約条件についての解がヌルストリングすなわち空っぽなストリングである場合、前記集合中に数値制約条件が全くなければ、前記集合は充足不能であり、そうでなければ前記集合中の数値制約条件が前記ヌルストリングによってさらに制約される。上記の逐次反復プロセスをさらに説明するために、例示的な制約条件の集合4を考える。ここで、sはストリングであり、abcdは整数である。この制約条件の集合を満たす解は、ストリングsおよび整数abcdについての五つの値の組み合わせであって、前記集合中の個々の制約条件すべてを同時に満足させるすなわち、すべての条件が真になるものがあることを意味する。より具体的には、制約条件sstartsWithを満たすためには、sの最初の三つのキャラクタがuvwでなければならない。制約条件sendsWithを満たすためには、sの最後の三つのキャラクタがxyzでなければならない。制約条件aslastIndexOfを満たすためには、sにおいてキャラクタtの最後の生起がaの値に等しいインデックス番号をもたなければならない。制約条件slength4を満たすためには、aおよびdの値の和は4以上でなければならない。制約条件c0を満たすためには、cの値は0より大きくなければならない。制約条件d7を意味する。制約条件aslastIndexOfは、sにおけるキャラクタtの最後の生起がaの値に等しいインデックス番号をもたなければならないことを要求する。tはsにおける最後のキャラクタではないので、これはa3であることも意味する。具体的実施形態は、sについての前記の解から導出される、abcに課される三つの追加的数値制約条件524を、もともと前記集合からの四つの数値制約条件522に追加して、もともと前記集合からの制約条件およびストリングsについての前記解から導出された制約条件を含む数値制約条件522、524すべてを満たすabcdについての値を見出すことを試みてもよい。ここでもまた、数値制約条件すべてを満たす整数abcdについての複数の値がある場合には、具体的実施形態は最も小さい値を最初に選択する。前記集合からの四つのもともとの数値制約条件522および上記の三つの追加的な、導出された数値制約条件524から、具体的実施形態は、abcdについての可能な解を、a=5b=7c=1d=-1として決定してもよい。実は、aについては、二つの可能な値5および6がある。値5が最小であり、よってaについてまず選択される。これら四つの値は、ストリング制約条件に対して検証されるために、ストリングドメイン510にフィードバックされる。第三の反復工程533では、第二の反復工程532の間に数値ドメイン520において見出されたabcdについての解が、ストリングドメイン510においてストリング制約条件に対して検証される。sがuvwtxyzであれば、aの値に等しいはずのtのインデックスは3なので、aは5に等しくなることはできない。aに対するこの新たな制約526すなわち、a5は、再び数値ドメイン520にフィードバックされる。第四の反復工程534の間、制約条件526、すなわちa5が他の既存の数値制約条件522、524に追加される。現在存在している数値制約条件522、524、526すべてを満たすabcdについての次の可能な解はa=6b=7c=1d=-1である。この解がストリングドメイン510にフィードバックされる。第五の反復工程535の間、前の反復工程の間に数値ドメイン520においてabcdについて見出された解すなわち、a=6b=7c=1d=-1が、同じようにして、ストリングドメイン510においてストリング制約条件に対して検証される。以前と同様、sがuvwtxyzであれば、aは6に等しくなることはできない。これはaに対する新たな制約条件528すなわち、a6を与え、数値ドメイン520にフィードバックされる。第六の反復工程536の間、再び、制約条件528、すなわちa6が他の既存の数値制約条件522、524、526に追加される。数値制約条件522、524、526、528すべてを満たす解を見出す試みがされる。ところが、現在存在している数値制約条件522、524、526、528すべてを満たすabcdについての値は存在しない。したがって、sがuvwtxyzであるとすると、すべての数値制約条件を満たすabcdについて見出すことのできる解は存在しない。この場合、sは、slength0という三つの制約条件のため、七個より多くのキャラクタをもつことはできない。より具体的には、c0なので、cがもちうる最小の値は1である。bcnknおよびk2である。第3行の分岐条件が満たされるためには、変数kの値が2より大きくなければならない。同様に、第3行の分岐条件が満たされる場合、第4行のコードが実行される。それ以外の場合には、第6~11行のコードが実行される。第6行では、第三の分岐点があり、分岐条件はnknmである。これも複数の下位条件たとえばnkおよびnmを含んでいる。第6行の分岐条件が満たされるためには、変数nの値が変数kの値または変数mの値に等しい必要がある。第6行の分岐条件が満たされる場合、第7行のコードが実行される。それ以外の場合、第9行のコードが実行される。さらに、第3行の条件分岐点は第1行の条件分岐点内にネストされており、第6行の条件分岐点は第3行の条件分岐点内にさらにネストされている。第1行の条件分岐点に付随する分岐条件が満たされない場合、このコードの実行中に第3行の条件分岐点に到達することは決してない。しかしながら、第3行の条件分岐点に付随する分岐条件が満たされない場合、第6行の条件分岐点はこのコードの実行中に到達される。実は、第6行の条件分岐点に到達するためには、第1行の分岐条件が満たされる必要があるが、第3行の分岐条件は満たされることができない。したがって、ソフトウェアモジュール中の各条件分岐点において、条件分岐点に付随する分岐条件が満たされるかどうかに依存して、ソフトウェアモジュールは異なる実行経路に沿って進む。図6は、複数レベルのネストされた条件分枝をもつ例示的ソフトウェアモジュールの実行経路を示している。条件分岐点602において、条件1が満たされる場合、実行経路は処理ステップ612のほうに進み、条件1が満たされない場合、実行経路は処理ステップ614のほうに進む。条件分岐点602内にネストされている条件分岐点604において、条件2が満たされる場合、実行経路は処理ステップ616のほうに進み、条件2が満たされない場合、実行経路は終了する。やはり条件分岐点602内にネストされている条件分岐点606では、条件3が満たされる場合、実行経路は終了し、条件3が満たされない場合、実行経路は条件分岐点608のほうに進む。条件分岐点606内にさらにネストされている条件分岐点608では、条件6が満たされる場合、実行経路は処理ステップ618のほうに進み、条件6が満たされない場合、実行経路は処理ステップ622のほうに進む。図6では、五つの可能な実行経路があり、ソフトウェアモジュールは、個々の条件分岐点602、604、606、608において分岐条件が満たされるかどうかに依存して、これら五つの可能な実行経路のうちのどの一つに沿って進むこともありうる。具体的実施形態は、分岐条件を、分岐条件を表す変数に課された数値制約条件またはストリング制約条件と考えてもよい。たとえば、サンプルコード1の第1行において、分岐条件はmnknと表現されてもよい。この制約条件の集合を満たすmnkについての任意の解は、この分岐条件が満たされるすなわち成り立つ結果につながり、ソフトウェアモジュールをある実行経路すなわち、コードのif部分に沿って進ませる。この分岐条件が満たされない場合は、mの値がnの値以下であるかkの値が10より大きいということである。これは、mnkに課される別の制約条件の集合として、と表現されてもよい。この第二の制約条件の集合を満たすmnkについての任意の解は、この分岐条件が満たされないすなわち偽になる結果につながり、ソフトウェアモジュールを別の実行経路すなわち、コードのelse部分に沿って進ませる。このように、具体的実施形態は、ソフトウェアモジュールにおける可能な各実行経路に対応する制約条件の集合を決定し、制約条件の各集合について一つまたは複数の解を見出し、該解を試験入力として使ってソフトウェアモジュールを試験してもよい。図7は、一つまたは複数の条件分岐点から帰結する複数の可能な実行経路を含むソフトウェアモジュールを試験する例示的な方法を示している。具体的実施形態では、ソフトウェアモジュールは任意の数の変数たとえば入力変数またはローカル変数および任意の数の条件分岐点たとえばifelse文を有していてもよい。各条件分岐点は、前記変数の一つまたは複数によって指定される分岐条件に関連付けられていてもよい。具体的実施形態では、分岐条件は任意の数の下位条件を含んでいてもよい。条件分岐点に付随する分岐条件が満たされるかどうかに依存して、ソフトウェアモジュールは異なる実行経路に沿って進んでもよい。具体的実施形態は、図7のステップ702に示されるように、ソフトウェアモジュールに対して記号的実行を行って、ソフトウェアモジュールの可能な各実行経路について、ソフトウェアモジュールをその実行経路に沿って進ませその実行経路の終わりに到達させる記号的表現の集合を決定してもよい。記号的表現の各集合を決定するとき、具体的実施形態は、もしあればソフトウェアモジュールの特定の諸変数に最初に課されていた数値制約条件およびストリング制約条件たとえば図1のステップ102との関連で述べたようなと、もしあればソフトウェアモジュールの特定の諸変数について推定された数値制約条件およびストリング制約条件たとえば図1のステップ104との関連で述べたようなとを組み込んでもよい。具体的実施形態では、図7のステップ702は図2に示されるシステム200のコンポーネント206によって実行されてもよい。これは、ソフトウェアモジュール212を入力として取り、ソフトウェアモジュール212に対して記号的実行を行い、ソフトウェアモジュール212の実行経路に対応する記号的表現の集合を出力として与えてもよい。コンピュータ科学の分野では、記号的実行symbolicexecutionとは、抽象解釈の場合として、実際の値ではなく記号的な値を追跡することによるソフトウェアプログラムの解析をいう。それは、ソフトウェアモジュールへの入力を記号変数として扱う、非明示的な状態モデル検査技法である。それは、記号的変数を用いてソフトウェアモジュール中のすべての有限経路を実行することによって複雑な数式もしくは表現を生成し、次いでもしあればエラーシナリオを得るためにソルバ典型的には決定手順decisionprocedureとして知られるを用いて複雑な式を解く。明示的な状態モデル検査とは対照的に、記号的実行は、解析対象のソフトウェアモジュールにおけるすべての入力変数のあらゆる可能な入力値およびあらゆる可能な使用ケースを計算することができる。記号的実行をさらに説明するために、fooと名付けられた例示的なソフトウェアモジュールを考える。ソフトウェアモジュールfooは二つの入力変数aおよびbおよび二つのローカル変数cおよびdをもつ。具体的実施形態では、ローカル変数の値は、直接または間接に、ソフトウェアモジュールの一つまたは複数の入力変数の値に依存する。たとえば、モジュールfooについては、ローカル変数cの値は、コードの第3行に示されるように、入力変数aおよびbの値に直接的に依存する。ローカル変数dの値は、コードの第5行に示されるように、ローカル変数cを通じて入力変数aおよびbの値に間接的に依存する。さらに、モジュールfooはコードの第4行にifelse文による条件分岐点を含む。第4行の条件分岐点は分岐条件に関連付けられている。この分岐条件が満たされるすなわち成り立つかどうか――すなわちローカル変数cがqrsに等しいかどうか――に依存して、モジュールfooは異なる実行経路を通って進み、モジュールfooのコードの異なる部分が実際には実行される。より具体的には、ローカル変数cがqrsに等しくない場合、コードの第5および6行に示されるように、ローカル変数dの値が計算され、返される。他方、ローカル変数cがqrsに等しい場合には、コードの第8行に示されるように、ローカル変数cが返される。記号的実行がモジュールfooに対して実行されるとき、その入力変数および出力変数はそれぞれ、実際の値の代わりに記号的な値を割り当てられる。図8は、モジュールfoo上で記号的実行を行うステップを表す例示的な実行フロー800を示している。この例では、入力変数aは記号的な値xを割り当てられ、入力変数bは記号的な値yを割り当てられ、ローカル変数cは記号的な値zを割り当てられ、ローカル変数dは記号的な値wを割り当てられる。変数abcdはstring型なので、記号的値xyzwはそれぞれ任意のストリングを表す。加えて、Φは、実行経路に沿ったさまざまな点における記号的実行の結果を表す記号的表現である。より具体的には、モジュールfooのコードの第2行に対応する802において、変数abcdはそれぞれの記号的値xyzwを割り当てられ、Φは初期には空またはヌル表現をもつ。実行がさらに進むにつれ、どのコードが実行されたかに依存してΦに表現が加えられていく。モジュールfooのコードの第3行に対応する804においては、Φは表現zconcatをもつ。コードの第3行がcaconcatであり、xyzがそれぞれ変数abcに割り当てられた記号的値だからである。次に、モジュールfooのコードの第4行は条件分岐点であり、実行が進みうる二つの可能な実行経路がある。よって、記号的実行も、804から二つの異なる経路を通って進みうる:第一の経路PATH1は、コードの第5および6行に対応する806および808を含み、第二の経路PATH2は、コードの第8行に対応する810を含む。PATH1を通って進むには、変数cはqrsに等しくない。これは、記号的値zがqrsに等しくないことを意味する。よって、表現zqrsが806においてΦに加えられる。逆に、PATH2を進むためには、変数cはqrsに等しい。これは、記号的値zがqrsに等しいことを意味する。よって、表現zqrsが810においてΦに加えられる。PATH1では、変数dの値が、808に対応するコードの第5行で決定される。したがって、表現wconcatが808においてΦに加えられる。zconcatなので、wについてのこの表現はwconcattと書き直してもよい。808はPATH1の終わりであり、よって808におけるΦの表現は、PATH1の実行の終わりに達するために満たされる必要のある、記号的な形での、条件を表している。同様に、810はPATH2の終わりであり、よって810におけるΦの表現は、PATH2の終わりに達するために満たされる必要のある、記号的な形での、条件を表している。モジュールfooは二つの可能な実行経路をもつので、モジュールfooを記号的に実行することは、結果として、各実行経路に対応して一つで、二組の表現を与える。具体的実施形態では、808におけるΦの表現について解くことは、モジュールfooにPATH1の終点に到達させる入力変数aおよびbについての実際の値を提供することができ、810におけるΦの表現について解くことは、モジュールfooにPATH2の終点に到達させる入力変数aおよびbについての実際の値を提供することができる。ソフトウェアモジュール上で記号的実行を行うことから帰結した表現のこれらの集合を解くには、具体的実施形態は、図7のステップ704に示されるように、表現の各集合を、ソフトウェアモジュールの変数に課される制約条件の集合として表してもよい。たとえば、モジュールfooでは、808における表現の集合は、abcdに対して課される制約条件の集合としてtと表されてもよい。810での表現の集合は、abcdに対して課される制約条件の集合としてと表されてもよい。ソフトウェアモジュールに対して記号的実行を行うことから得られる制約条件の各集合について、具体的実施形態は、該集合からの各数値制約条件を適用可能な数式として表し、該集合からの各ストリング制約条件をアプリケーションFSMとして表してもよい。図9Aは、例示的なソフトウェアモジュールについて決定された三つの例示的な制約条件の集合902、904、906を、該ソフトウェアモジュールの三つの対応する実行経路912、914、916とともに示している。ここで、数値制約条件は数式として表され、ストリング制約条件はFSMとして表されている。この例示的なソフトウェアモジュールを試験するため、各経路912、914、916の終わりにおいて、制約条件のそれぞれの対応する集合902、906、906が試験ケースについて解かれる。次いで、具体的実施形態は、図7のステップ706に示されるように、図1に示されるプロセスを使って、制約条件の各集合について一つまたは複数の解を見出すことを試み、図7のステップ708に示されるように、見出された解を試験入力として使ってソフトウェアモジュールを試験してもよい。具体的実施形態では、制約条件の集合についての解は、制約条件が課されている変数についての実際の値であって、該集合内のすべての制約条件を満たすものを含みうる。ソフトウェアモジュールを試験するときは、これらの実際の解の値は、試験入力としてソフトウェアモジュールの変数に代入されてもよい。制約条件のある集合について見出された解が与えられたとき、その解の諸値は一緒になって対応する制約条件の集合からのすべての制約条件を満たし、制約条件の集合は、ソフトウェアモジュールが特定の実行経路に沿って進み、該特定の実行経路の終わりに達する際に、該ソフトウェアモジュールの状態を表す表現の集合たとえば記号的実行から得られたに対応するので、実際の値すなわち、制約条件の前記集合について見出された解からの値のこの特定の組み合わせを試験入力としてソフトウェアモジュールに適用することによって、ソフトウェアモジュールが前記特定の実行経路に沿って進み、前記特定の実行経路の終わりに達することが保証される。結果として、これは、これらの特定の解の値がソフトウェアモジュールの対応する変数に試験入力として代入されれば前記特定の実行経路がフルに試験されるということを意味する。さらに、ソフトウェアモジュールの一つ一つのすべての実行経路について得られる表現の一つ一つのすべての集合に対応する制約条件の一つ一つのすべての集合について、解を見出すことができ、解の値がソフトウェアモジュールに試験入力として適用されるたとえば一つの解の実際の諸値を同時に適用することによってならば、ソフトウェアモジュールのすべての可能な実行経路がフルに試験されうる。ソフトウェアモジュールの実行経路のいずれかにおいて何らかのエラーがある場合、そのような系統的な試験は最終的にはそのようなエラーを捕捉できることがありうる。具体的実施形態では、図1に示されるようなプロセスが、ソフトウェアモジュールの設計条件または仕様要件が満たされているかどうかを検証するために使用されうる。典型的には、任意の所与のソフトウェアモジュールに関連付けられた形式的な設計要件または仕様要件があってもよい。これらの形式的な要件のいくつかは、ソフトウェアモジュールの入力または出力に課されてもよい。個別的実施形態では、ソフトウェアモジュールの入力に課される仕様要件は、そのソフトウェアモジュールに関連する事前条件と称されてもよく、ソフトウェアモジュールの出力に課される仕様要件は、そのソフトウェアモジュールに関連する事後条件と称されてもよい。時に、事後条件は、そのソフトウェアモジュールに関連する事前条件に依存してもよい。上で説明したように、しばしば、ソフトウェアモジュールは、任意の数の条件分岐点たとえばifelse文を含んでいてもよく、各条件分岐点はソフトウェアモジュールの一つまたは複数の変数たとえば入力変数またはローカル変数によって指定される分岐条件をもつ。分岐条件が満たされるかどうかに依存して、ソフトウェアモジュールは異なる実行経路を進みうる。よって、ソフトウェアモジュールが実行されるとき、ソフトウェアモジュールに含まれる条件分岐点から帰結する可能な実行経路のうちのいずれを進んでもよい。結果として、具体的実施形態では、ソフトウェアモジュールがその入力および出力に課される形式的な仕様要件すなわち、そのソフトウェアモジュールに関連する事前条件および事後条件を満たすかどうかを検証する際、ソフトウェアモジュールが検証試験に合格するすなわち、仕様要件を満たすと考えられるのは、そのソフトウェアモジュールに関連するすべての事前条件および事後条件が、そのソフトウェアモジュールのすべての可能な実行経路について成り立つ場合であり、かつその場合に限られる。図10は、ソフトウェアモジュールの入力および出力に課される要件たとえば形式的な設計要件または仕様要件すなわち、ソフトウェアモジュールに関連する事前条件および事後条件との関連でソフトウェアモジュールを検証する例示的な方法を示している。図10のステップ1002に示されるように、具体的実施形態は、ソフトウェアモジュールの各事前条件たとえば、入力変数に課される要件および各事後条件たとえば出力変数に課される要件を、ソフトウェアモジュールの入力変数または出力変数に課される制約条件として表してもよい。たとえば、ストリング型の二つの入力変数aおよびbをもつ先の例示的なソフトウェアモジュールfooを考える。上に示したfooのコードに基づいて、fooがストリング型の一つの出力値を返すことが判別されうる。たとえばソフトウェアモジュールfooの仕様によって指定され、abpに課される制約条件として表されるabpに課される事前条件および事後条件は次のようになる。次いで具体的実施形態は、図10のステップ1004に示されるように、ソフトウェアモジュールの事後条件を否定にしてもよい。上の例では、ソフトウェアモジュールは一つの事後条件pendsWithをもつ。この事後条件の論理的な否定は、となる。具体的実施形態は、図10のステップ1006に示されるように、ソフトウェアモジュールに対して記号的実行を行って、ソフトウェアモジュールの可能な各実行経路に対応する制約条件の集合を得、次いで、事前条件および否定にされた事後条件を制約条件の各集合に組み込んでもよい。記号的実行は、図7のステップ702との関連で上述してあり、ここでも同様に実行されてもよい。制約条件の各集合を決定するとき、具体的実施形態は、もしあればソフトウェアモジュールの個別的な変数に最初に課されていた数値およびストリング制約条件図1のステップ102との関連で述べたようなならびにもしあればソフトウェアモジュールの個別的な変数について推定された数値およびストリング制約条件図1のステップ104との関連で述べたようなを組み込んでもよい。たとえば、ソフトウェアモジュールfooは、図8に示されるように、二つの可能な実行経路をもつ。こうして、ソフトウェアモジュールfooに対して記号的実行を行うことは、結果として二組の表現を与える。第一の経路PATH1については、fooに対して記号的実行を行うことから得られる表現の集合は、図8の808によって示されるように、tqrsと書いてもよい。pはPATH1についてはdの値をもつことを注意しておく。dがPATH1の終わりにfooによって返される値すなわちfooの出力であり、wはdに割り当てられた記号的値だからである。さらに、xがaに割り当てられた記号的値なのでaはxと等価であり、bはyと等価であり、zはcと等価であり、cはfooのソースコードによればconcatに等しい。次いで、事前条件および否定にされた事後条件はこの制約条件の集合に加えられてもよい。よって、PATH1についての最終的な制約条件の集合は、tqrsとなる。第二の経路PATH2については、fooに対して記号的実行を行うことから得られる表現の集合は、図8の810によって示されるように、qrsと書いてもよい。pはPATH2についてはcの値をもつことを注意しておく。cがPATH2の終わりにfooによって返される値すなわちfooの出力であり、zはcに割り当てられた記号的値だからである。cはfooのソースコードによればconcatに等しい。事前条件および否定にされた事後条件はこの制約条件の集合に同様に加えられてもよい。PATH2についての最終的な制約条件の集合は、qrsとなる。次いで具体的実施形態は、図10の1008に示されるように、図1に示されるプロセスを使って、ソフトウェアモジュールの可能な各実行経路に対応する制約条件の各集合について、一つまたは複数の解を見出すことを試みてもよい。制約条件の各集合は、ソフトウェアモジュールに対して記号的実行を行うことから得られる制約条件と、ソフトウェアモジュールに関連する事前条件および否定にされた事後条件とを含む。具体的実施形態では、ソフトウェアモジュールの個別的な特定の実行経路に対応する制約条件の各集合について、前記集合からのすべての制約条件を満たす解が見出され得ない場合、この実行経路については、ソフトウェアモジュールは、事前条件および事後条件によって表される入力および出力に課される要件を満たす。図10のステップ1004および1006で説明されたように、制約条件の各集合はソフトウェアモジュールの出力に課される否定にされた事後条件を含むことを想起されたい。よって、制約条件の集合について解が見出され得ないすなわち、その制約条件の集合が充足不能である場合、特に事後条件の否定を満たす解が見出され得ない場合、それは、対応する実行経路について事前条件および事後条件が成り立つということを意味する。逆に、前記集合からの制約条件すべてを満たす何らかの解が見出されうる場合には、対応する実行経路について、ソフトウェアモジュールはその入力および出力に課される要件を満たさない。その実行経路については事前条件および事後条件が成り立たないからである。したがって、図10のステップ1006において得られた制約条件の任意の集合について何らかの解が見出されうる場合、ソフトウェアモジュールは、その入力および出力に課される要件に関して検証試験に合格しない。図10のステップ1006で得られる制約条件の一つ一つのすべての集合が充足不能であるときにのみ、ソフトウェアモジュールは、その入力および出力に課される要件に関して検証試験に合格する。図9Bは、図9Aに示した、前記例示的なソフトウェアモジュールについて決定された制約条件の三つの例示的な集合902、904、906を、ソフトウェアモジュールの三つの対応する実行経路912、914、916とともに再度示している。この例示的なソフトウェアモジュールを、該ソフトウェアモジュールの入力および出力に課される要件との関連で検証するには、各経路912、914、916の終わりにおいて、制約条件の各対応する集合902、904、906が要件および主張について解かれる。具体的実施形態では、図1に示されるようなプロセスが、インジェクション攻撃を検出および捕捉するよう設計されたソフトウェアモジュールを検証するために使用されてもよい。挿入攻撃としても知られるインジェクション攻撃は、しばしばSQLデータベースおよび他の脆弱なウェブサイトを標的にする悪意のあるソフトウェア攻撃の一形である。一般に、SQLインジェクションは、ソフトウェアアプリケーションのデータベース層に存在するセキュリティ上の脆弱性を活用するコード注入技法である。脆弱性は、プログラミングまたはスクリプティング言語が別のプログラミングまたはスクリプティング言語内に埋め込まれるときに常に起こりうる。より具体的には、脆弱性が存在しうるのは、ユーザー入力がSQL文に埋め込まれたストリングリテラルのエスケープキャラクタについて誤ったフィルタリングがされたとき、あるいはユーザー入力が強く型指定されず、そのため予期せずに実行されるときである。たとえば、インジェクション攻撃は、ストリングshutdownを別のストリングたとえばランダムな文字の集合にqkd1shutdownsqdとして埋め込み、このストリングを入力コマンドSQL文としてデータベースに送ることがある。データベースソフトウェアが、一見ランダムな入力ストリングに埋め込まれているshutdownストリングを捕捉せずに実行してしまうと、shutdownシャットダウンストリングがデータベースを意図せずしてシャットダウンさせてしまうことがありうる。このため、たいていのデータベースは、そのようなインジェクション攻撃を検出および捕捉するよう設計されたソフトウェアモジュールを有する。具体的実施形態では、図1に示されるプロセスが、そのようなセキュリティソフトウェアモジュールが、インジェクション攻撃として入力に埋め込まれうる悪意のあるストリングの多くの異なる形を検出できるかどうかを、検証するために使用されてもよい。たとえば、セキュリティソフトウェアモジュールを試験する一つの方法は、そのセキュリティソフトウェアモジュールが検出できないようたとえば、セキュリティソフトウェアモジュールをだましてその悪意のあるストリングが無害であると思い込ませるよう悪意のあるストリングまたは悪意のあるストリングを埋め込む方法を考案することでありうる。図11は、インジェクション攻撃を検出するよう設計されたセキュリティソフトウェアモジュールを検証する例示的な方法を示している。具体的実施形態では、セキュリティソフトウェアモジュールは、入力ストリングが何らかの悪意のあるストリングを含むかどうかを検証するために、セキュリティソフトウェアモジュールに渡される入力値たとえば入力ストリングに対してさまざまなセキュリティ検査を実行してもよい。各セキュリティチェックポイントにおいて、入力値がセキュリティ検査を通過した場合には、セキュリティソフトウェアモジュールは次のセキュリティチェックポイントに進んでもよい。それ以外の場合には、セキュリティソフトウェアモジュールは、入力値が特定のセキュリティ検査に不合格だったとの指示を返してもよいたとえばFALSEを返す。入力ストリングが、セキュリティソフトウェアモジュールに含まれるすべてのセキュリティ検査を通過した場合にのみ、セキュリティソフトウェアモジュールは、入力値が無害であるとの指示を返すたとえば、TRUEを返す。具体的実施形態は、図11のステップ1102に示されるように、インジェクション攻撃との関連で使われそうな、shutdownのような悪意のあるストリングの集合を選択してもよい。mがある特定の悪意のあるストリングを表すとする。次いで、具体的実施形態は、図11のステップ1104に示されるように、前記集合からのそれぞれの悪意のあるストリングをsで表される別のストリングに埋め込んでもよい。sにおいては、悪意のあるストリングの前のいくつかのキャラクタすなわち部分ストリングおよび悪意のあるストリングの後のいくつかのキャラクタすなわち別の部分ストリングがあってもよい。このように、sは、sconcatyと表されうる。ここで、sにおいて、xは悪意のあるストリングmの前の部分ストリングを表し、yは悪意のあるストリングmの後の部分ストリングを表す。xもyも空ストリングであってもよく、mがsの別の部分ストリングになることを注意しておく。次いで、ストリンsはセキュリティソフトウェアモジュールに入力値として加えられてもよい。具体的実施形態は、図11のステップ1106に示されるように、セキュリティソフトウェアモジュールに関して記号的実行を行って制約条件の集合を得てもよい。該制約条件の集合は、満足されれば、セキュリティソフトウェアモジュールに終わりまで実行させ、入力値がそこに含まれるすべてのセキュリティ検査に合格したとの指示を返させるたとえばTRUEを返すものである。記号的実行は、図7のステップ702との関連で上記してあり、ここでも同様に実行されてもよい。制約条件の集合を決定するとき、具体的実施形態は、もしあればソフトウェアモジュールの個別的な変数に最初に課されていた数値およびストリング制約条件図1のステップ102との関連で述べたようなならびにもしあればソフトウェアモジュールの個別的な変数について推定された数値およびストリング制約条件図1のステップ104との関連で述べたようなを組み込んでもよい。具体的実施形態では、こうして得られた制約条件の集合は、セキュリティソフトウェアモジュールに含まれるすべてのセキュリティ検査に合格してソフトウェアモジュールが入力値が無害であることを示す出力値を返すために、セキュリティソフトウェアモジュールの入力変数に代入された入力値について満足される必要のある制約条件すべてを表す。具体的実施形態は、図11のステップ1108に示されるように、図1に示されるプロセスを使って、sがすべての制約条件を満たすよう、各悪意のあるストリングが埋め込まれているsについての一つまたは複数の解を見出すことを試みてもよい。sについて制約条件の集合を満たす何らかの解が見出されうる場合、それは、セキュリティソフトウェアモジュールに含まれるすべてのセキュリティ検査をすり抜けうる、sに埋め込まれた少なくとも一つの悪意のあるストリングがあることを意味する。その結果、セキュリティソフトウェアモジュールはインジェクション攻撃に対して脆弱である。悪意のあるストリングshutdownを例として使う。このストリングをsに埋め込むと、結果はsconcatyとなる。図1に示したプロセスを使って、具体的実施形態は、shutdownが埋め込まれたsがセキュリティソフトウェアモジュールに関する記号的実行を行うことから得られる制約条件の集合からのすべての制約条件を満たしうるよう、部分ストリングxおよびyの値を与えるsについての何らかの解があるかどうかを見出そうと試みてもよい。xおよびyについての解があれば、それは、ストリングsがセキュリティソフトウェアモジュールに含まれるすべてのセキュリティ検査に合格できるようにすなわち、セキュリティソフトウェアモジュールが悪意のあるストリングshutdownを埋め込まれたその特定のインジェクション攻撃を検出し損なうように、値concatyをもつストリングs中に悪意のあるストリングshutdownを埋め込む少なくとも一つの方法があることを意味する。具体的実施形態では、各悪意のあるストリングは、ストリングsに埋め込まれるとき、異なるデータ型を使って表されることがある。たとえば、ストリングshutdownを十六進数として表すと、0x73687574646f766eである。このように、sについての一つの可能な値は、ストリングデータ型でこの悪意のあるストリングを表すexecshutdownでありうる。一方、sについての別の可能な値は、整数データ型でこの悪意のあるストリングを表すdeclareacharselecta0x73687574646f766eexecでありうる。具体的実施形態は、埋め込まれた悪意のあるストリングが異なるデータ型を使って表される場合にsについての解を見出そうと試みてもよい。結果として、セキュリティソフトウェアモジュールは、通常のストリングデータ型として表された悪意のあるストリングに関して試験されるだけでなく、予期されないデータ型で表されたたとえば整数または浮動小数点数として表された悪意のあるストリングに関しても試験される。具体的実施形態は、悪意のあるストリングの集合からの各悪意のあるストリングmをsに埋め込み、次いで、ストリング全体としてのすなわちxmおよびyを含むsが図11のステップ1106から得られた制約条件の集合を満たすような、xおよびyについての特定の値を与えるsについての解を見出そうと試みてもよい。埋め込まれた何らかの悪意のあるストリングmをもつsについての何らかの解が見出されうる場合、それは、そのセキュリティソフトウェアモジュールは対応するインジェクション攻撃を検出できず、よって脆弱であることを意味する。さらに、埋め込まれた何らかの悪意のあるストリングmをもつsについての何の解も見出されえない場合、具体的実施形態はさらに、図11のステップ1106から得られる制約条件の集合を満たす解を見出そうと試みてもよい。何らかの解が見出されうる場合、具体的実施形態は、その解自身が実際に悪意のあるストリングであるかどうかを検証してもよい。セキュリティソフトウェアモジュールに対するこの検証は、悪意のあるストリングが、別のストリングに埋め込まれることなくそれ自身で、セキュリティソフトウェアモジュールに含まれるすべてのセキュリティ検査を合格できるかどうかすなわち、セキュリティソフトウェアモジュールが何らかの悪意のあるストリングを検出し損なうかどうかを判定するよう試みる。図9Cは、図9Aに示した、前記例示的なソフトウェアモジュールについて決定された制約条件の三つの例示的な集合902、904、906を、ソフトウェアモジュールの三つの対応する実行経路912、914、916とともに再度示している。この例示的なソフトウェアモジュールが例示的なセキュリティソフトウェアモジュールである場合、この例示的なセキュリティソフトウェアモジュールを検証するには、各経路912、914、916の終わりにおいて、制約条件の各対応する集合902、904、906が、当該ソフトウェアの内部検査を通過したあらゆる可能なストリングを表すホットスポットFSM有限状態機械と、悪意のあるFSMとの交わりについて、解かれる。交わりがヌルであれば、可能なインジェクション攻撃は一つも見出されることができない。ヌルでない交わりは、ただちに可能なインジェクション攻撃ストリングを指し示す。具体的実施形態は、ネットワーク環境において実装されてもよい。図12は、サービスとしてソフトウェア検証を提供するのに好適な例示的なネットワーク環境1200を示している。ネットワーク環境1200は、一つまたは複数のサーバー1220および一つまた複数のクライアント1230を互いに結合するネットワーク1210を含む。具体的実施形態では、ネットワーク1210はイントラネット、エクストラネット、仮想閉域網VPNvirtualprivatenetwork、ローカルエリアネットワークLANlocalareanetwork、無線LANWLANwirelessLAN、広域ネットワークWANwideareanetwork、都市圏ネットワークMANmetropolitanareanetwork、インターネットの一部または別のネットワーク1210または二つ以上のそのようなネットワーク1210の組み合わせである。本開示は、任意の好適なネットワーク1210を考えている。一つまたは複数のリンク1250はサーバー1220またはクライアント1230をネットワーク1210に結合する。具体的実施形態では、一つまたは複数のリンク1250はそれぞれ一つまたは複数の有線、無線または光学式リンク1250を含む。具体的実施形態では、一つまたは複数のリンク1250はそれぞれ、イントラネット、エクストラネット、VPN、LAN、WLAN、WAN、MAN、インターネットの一部または別のリンク1250または二つ以上のそのようなリンク1250の組み合わせを含む。本開示は、サーバー1220およびクライアント1230をネットワーク1210に結合する任意の好適なリンク1250を考えている。具体的実施形態では、各サーバー1220は単体のサーバーであってもよいし、あるいは複数のコンピュータまたは複数のデータセンターにまたがる分散式のサーバーであってもよい。サーバー1220はさまざまな型でありえ、たとえば、限定するものではないが、ウェブサーバー、ニュースサーバー、メールサーバー、メッセージサーバー、広告サーバー、ファイルサーバー、アプリケーションサーバー、交換サーバー、データベースサーバーまたはプロキシサーバーといったものでありうる。具体的実施形態では、各サーバー1220は、サーバー1220によって実装またはサポートされる適切な機能を実行するために、ハードウェア、ソフトウェアまたは埋め込まれた論理コンポーネントまたは二つ以上のそのようなコンポーネントの組み合わせを含んでいてもよい。たとえば、ウェブサーバーは一般に、ウェブページまたはウェブページの個別的な要素を含むウェブサイトをホストすることができる。より具体的には、ウェブサーバーはHTMLファイルまたは他のファイル型をホストしてもよく、あるいは要求に際してファイルを動的に生成または構築し、クライアント1230からのHTTPまたはその他の要求に応答してそれをクライアント1230に通信してもよい。メールサーバーは一般にさまざまなクライアント1230に電子メールサービスを提供することができる。データベースサーバーは一般に、一つまたは複数のデータストアに記憶されたデータを管理するためのインターフェースを提供することができる。具体的実施形態では、一つまたは複数のデータ記憶装置1240が一つまたは複数のリンク1250を介して一つまたは複数のサーバー1220に通信上リンクされてもよい。具体的実施形態では、データ記憶装置1240はさまざまな型の情報を記憶するために使用されうる。具体的実施形態では、データ記憶装置1240に記憶される情報は、特定のデータ構造に従って編成されてもよい。具体的実施形態では、各データ記憶装置1240はリレーショナルデータベースであってもよい。具体的実施形態は、サーバー1220またはクライアント1230がデータ記憶装置1240に記憶されている情報を管理する、たとえば取得、修正、追加または削除することができるようにするインターフェースを提供してもよい。具体的実施形態では、各クライアント1230は、ハードウェア、ソフトウェアまたは埋め込まれた論理コンポーネントまたは二つ以上のそのようなコンポーネントの組み合わせを含み、クライアント1230によって実装またはサポートされる適切な機能を実行することができる電子装置であってもよい。たとえば、限定するものではないが、クライアント1230はデスクトップコンピュータシステム、ノートブックコンピュータシステム、ハンドヘルド電子装置または携帯電話であってもよい。本開示は、任意の好適なクライアント1230を考えている。クライアント1230は、クライアント1230のところにいるネットワークユーザーが、ネットワーク1210にアクセスできるようにしてもよい。クライアント1230は、そのユーザーが他のクライアント1230のところにいる他のユーザーと通信できるようにしてもよい。クライアント1230は、マイクロソフトインターネットエクスプローラー、グーグルクロームまたはモジラファイアフォックスのようなウェブブラウザー1232を有していてもよく、一つまたは複数のアドオン、プラグインまたはツールバーまたはヤフーツールバーのような他の拡張を有していてもよい。クライアント1230のところにいるユーザーは一様リソース位置指定子URLUniformResourceLocatorまたはウェブブラウザー1232にサーバー1220を指定する他のアドレスを入力してもよく、ウェブブラウザー1232はハイパーテキスト転送プロトコルHTTPHyperTextTransferProtocol要求を生成し、該HTTP要求をサーバー1220に通信してもよい。サーバー1220はHTTP要求を受け容れ、該HTTP要求に応答してクライアント1230に一つまたは複数のハイパーテキストマークアップ言語HTMLHyperTextMarkupLanguageファイルを通信してもよい。クライアント1230は、サーバー1220からのHTMLファイルに基づいて、ユーザーへの呈示のためにウェブページをレンダリングしてもよい。本開示は、任意の好適なウェブページファイルを考えている。一例として、限定するわけではないが、ウェブページは個別のニーズに応じて、HTMLファイル、拡張可能ハイパーテキストマークアップ言語XHTMLExtensibleHyperTextMarkupLanguageファイルまたは拡張可能マークアップ言語XMLExtensibleMarkupLanguageファイルからレンダリングしてもよい。そのようなページはまた、スクリプトを実行してもよい。スクリプトは、たとえば、限定するものではないが、ジャバスクリプト、ジャバ、マイクロソフトシルバーライトSILVERLIGHT、AJAXAsynchronousJAVASCRIPTandXMLのようなマークアップ言語およびスクリプトの組み合わせで書かれたものなどである。本稿では、適宜、ウェブページへの言及は、一つまたは複数の対応するブラウザーがウェブページをレンダリングするために使うことができるウェブページファイルを包含し、逆もまたしかりであるつまり、ウェブページファイルへの言及は一つまたは複数の対応するウェブページを包含する。具体的実施形態は、一つまたは複数のコンピュータシステム上で実装されてもよい。図13は、例示的なコンピュータシステム1300を示している。具体的実施形態では、一つまたは複数のコンピュータシステム1300が、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行する。具体的実施形態では、一つまたは複数のコンピュータシステム1300は本願で記載または図示される機能を実行する。具体的実施形態では、一つまたは複数のコンピュータシステム1300上で走るソフトウェアが本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行し、あるいは本願で記載または図示される機能を提供する。具体的実施形態は、一つまたは複数のコンピュータシステム1300の一つまたは複数の部分を含む。本開示は、任意の好適な数のコンピュータシステム1300を考えている。本開示は、任意の好適な物理的形態を取るコンピュータシステム1300を考えている。例として、限定するわけではないが、コンピュータシステム1300は組み込みコンピュータシステム、システムオンチップSOCsystemonchip、単一ボードコンピュータシステムSBCsingleboardcomputersystemたとえばコンピュータオンモジュールCOMcomputeronmoduleまたはシステムオンモジュールSOMsystemonmoduleのような、デスクトップコンピュータシステム、ラップトップまたはノートブックコンピュータシステム、対話的キオスク、メインフレーム、コンピュータシステムのメッシュ、携帯電話、携帯情報端末PDApersonaldigitalassistant、サーバーまたはこれらの二つ以上の組み合わせであってもよい。適宜、コンピュータシステム1300は一つまたは複数のコンピュータシステム1300を含んでいてもよいし、単体でも分散式でもよいし、複数の位置にまたがってもよいし、複数の機械にまたがってもよいし、クラウドに存在してもよい。クラウドは、一つまたは複数のネットワークにおける一つまたは複数のクラウドコンポーネントを含んでいてもよい。適宜、一つまたは複数のコンピュータシステム1300は、実質的な空間的または時間的制約なしに、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行してもよい。一例として、限定するわけではないが、一つまたは複数のコンピュータシステム1300は、リアルタイムで、あるいはバッチモードで、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行してもよい。一つまたは複数のコンピュータシステム1300は、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを、適切であれば異なる複数の時間に、あるいは異なる複数の位置で、実行してもよい。具体的実施形態では、コンピュータシステム1300はプロセッサ1302、メモリ1304、記憶装置1306、入出力IOインターフェース1308、通信インターフェース1310およびバス1312を含む。本開示は具体的な数の具体的なコンポーネントを具体的な構成で有する具体的なコンピュータシステムを記載および図示しているが、本開示は任意の好適な数の任意の好適なコンポーネントを任意の好適な構成で有する任意の好適なコンピュータシステムを考えている。具体的実施形態では、プロセッサ1302は、コンピュータプログラムをなす命令のような命令を実行するためのハードウェアを含む。一例として、限定するわけではないが、命令を実行するために、プロセッサ1302は内部レジスタ、内部キャッシュ、メモリ1304または記憶装置1306から命令を取得またはフェッチし、それらの命令をデコードおよび実行し、次いで一つまたは複数の結果を内部レジスタ、内部キャッシュ、メモリ1304または記憶装置1306に書き込んでもよい。具体的実施形態では、プロセッサ1302はデータ、命令またはアドレスのための一つまたは複数の内部キャッシュを含んでいてもよい。本開示は、適宜、任意の好適な数の任意の好適な内部キャッシュを含むプロセッサ1302を考えている。一例として、限定するわけではないが、プロセッサ1302は一つまたは複数の命令キャッシュ、一つまたは複数のデータキャッシュおよび一つまたは複数のトランスレーションルックアサイドバッファTLBtranslationlookasidebufferを含んでいてもよい。命令キャッシュ中の命令は、メモリ1304または記憶装置1306中の命令のコピーであってもよく、命令キャッシュはプロセッサ1302によるそれらの命令の取得を高速化しうる。データキャッシュ中のデータはプロセッサ1302で実行中の命令が作用するメモリ1304または記憶装置1306中のデータのコピーであってもよく、プロセッサ1302で実行されるその後の命令によるアクセスのためまたはメモリ1304もしくは記憶装置1306への書き込みのための、プロセッサ1302で実行された前の命令の結果であってもよく、他の好適なデータであってもよい。データキャッシュは、プロセッサ1302による読み出しまたは書き込み動作を高速化しうる。TLBは、プロセッサ1302のための仮想アドレス変換を高速化しうる。具体的実施形態では、プロセッサ1302は、データ、命令またはアドレスのための一つまたは複数の内部レジスタを含んでいてもよい。本開示は、適宜、任意の好適な数の任意の好適な内部レジスタを含むプロセッサ1302を考えている。適切な場合には、プロセッサ1302は、一つまたは複数の算術論理ユニットALUarithmeticlogicunitを含んでいてもよく、マルチコアプロセッサであってもよく、一つまたは複数のプロセッサ1302を含んでいてもよい。本開示は具体的なプロセッサを記載および図示しているが、本開示は任意の好適なプロセッサを考えている。具体的実施形態では、メモリ1304は、プロセッサ1302が実行するための命令およびプロセッサ1302が作用するためのデータを記憶するためのメインメモリを含む。一例として、限定するわけではないが、システム1300は記憶装置1306または他の源たとえば別のコンピュータシステム1300のようなから命令をメモリ1304にロードしてもよい。プロセッサ1302は次いでメモリ1304からの命令を内部レジスタまたは内部キャッシュにロードしてもよい。命令を実行するために、プロセッサ1302は内部レジスタまたは内部キャッシュから命令を取得し、それをデコードしてもよい。命令の実行中または実行後に、プロセッサ1302は一つまたは複数の結果これは中間結果であってもよいし、最終結果であってもよいを内部レジスタまたは内部キャッシュに書き込んでもよい。プロセッサ1302は次いでそれらの結果のうちの一つまたは複数をメモリ1304に書き込んでもよい。具体的実施形態では、プロセッサ1302は、記憶装置1306その他の箇所ではなく一つまたは複数の内部レジスタまたは内部キャッシュ内またはメモリ1304内の命令のみを実行し、記憶装置1306その他の箇所ではなく一つまたは複数の内部レジスタまたは内部キャッシュ内またはメモリ1304内のデータに対してのみ演算する。一つまたは複数のメモリバスこれはそれぞれアドレスバスおよびデータバスを含んでいてもよいがプロセッサ1302をメモリ1304に結合してもよい。バス1312は後述するように一つまたは複数のメモリバスを含んでいてもよい。具体的実施形態では、一つまたは複数のメモリ管理ユニットMMUmemorymanagementunitがプロセッサ1302とメモリ1304との間に存在し、プロセッサ1302によって要求されるメモリ1304へのアクセスを容易にする。具体的実施形態では、メモリ1304はランダムアクセスメモリRAMを含む。このRAMは適切であれば揮発性メモリであってもよい。適切であれば、このRAMは動的RAMDRAMまたは静的RAMSRAMであってもよい。さらに、適切であれば、このRAMは単一ポートまたはマルチポートのRAMであってもよい。本開示は任意の好適なRAMを考えている。メモリ1304は適宜一つまたは複数のメモリ1304を含んでいてもよい。本開示は具体的なメモリを記述および図示しているが、本開示は任意の好適なメモリを考えている。具体的実施形態では、記憶装置1306はデータまたは命令についての大容量記憶装置を含む。一例として、限定するわけではないが、記憶装置1306はHDD、フロッピーディスクドライブ、フラッシュメモリ、光ディスク、光磁気ディスク、磁気テープまたはユニバーサルシリアルバスUSBUniversalSerialBusドライブまたはこれらのうち二つ以上の組み合わせを含んでいてもよい。記憶装置1306は、適宜、リムーバブルまたは非リムーバブルなすなわち固定式のメディアを含んでいてもよい。記憶装置1306は適宜コンピュータシステム1300の内部または外部であってもよい。具体的実施形態では、記憶装置1306は不揮発性の半導体メモリであってもよい。具体的実施形態では、記憶装置1306は読み出し専用メモリROMを含む。適切であれば、このROMはマスクプログラムされたROM、プログラム可能型ROMPROM、消去可能型PROMEPROM、電気的消去可能型EPROMEEPROM、電気的変更可能型ROMEAROMまたはフラッシュメモリまたはこれらのうち二つ以上の組み合わせであってもよい。本開示は、任意の好適な物理的形態を取る大容量記憶装置1306を考えている。記憶装置1306は、適宜、プロセッサ1302と記憶装置1306の間の通信を容易にする一つまたは複数の記憶装置制御ユニットを含んでいてもよい。適切であれば、記憶装置1306は一つまたは複数の記憶装置1306を含んでいてもよい。本開示は具体的な記憶装置を記載および図示するが、本開示は任意の好適な記憶装置を考えている。具体的実施形態では、IOインターフェース1308は、コンピュータシステム1300と一つまたは複数のIO装置との間の通信のための一つまたは複数のインターフェースを提供するためのハードウェア、ソフトウェアまたはその両方を含む。コンピュータシステム1300は適宜、これらのIO装置の一つまたは複数を含んでもよい。これらのIO装置の一つまたは複数は、人とコンピュータシステム1300の間の伝達を可能にしうる。一例として、限定するわけではないが、IO装置はキーボード、キーパッド、マイクロホン、モニタ、マウス、プリンタ、スキャナ、スピーカー、スチールカメラ、スタイラス、タブレット、タッチスクリーン、トラックボール、ビデオカメラ、他の好適なIO装置またはこれらのうちの二つ以上の組み合わせを含んでいてもよい。IO装置は一つまたは複数のセンサーを含んでいてもよい。本開示は任意の好適なIO装置およびそのための任意の好適なIOインターフェース1308を考えている。適切であれば、IOインターフェース1308は、プロセッサ1302がこれらのIO装置の一つまたは複数を駆動できるようにする一つまたは複数の装置またはソフトウェアドライバを含んでいてもよい。IOインターフェース1308は、適宜、一つまたは複数のIOインターフェースを含んでいてもよい。本開示は具体的なIOインターフェースを記載および図示しているが、本開示は任意の好適なIOインターフェースを考えている。具体的実施形態では、通信インターフェース1310は、コンピュータシステム1300と一つまたは複数の他のコンピュータシステム1300または一つまたは複数のネットワークとの間の通信たとえばパケットベースの通信のための一つまたは複数のインターフェースを提供するハードウェア、ソフトウェアまたはその両方を含む。一例として、限定するわけではないが、通信インターフェース1310は、イーサネットまたは他の有線ベースのネットワークと通信するためのネットワークインターフェースコントローラNICnetworkinterfacecontrollerまたはネットワークアダプター、あるいはWIFIネットワークのような無線ネットワークと通信するための無線NICWNICまたは無線アダプターを含んでいてもよい。本開示は任意の好適なネットワークおよびそのための任意の好適な通信インターフェース1310を考えている。一例として、限定するわけではないが、コンピュータシステム1300はアドホックネットワーク、パーソナルエリアネットワークPAN、ローカルエリアネットワークLAN、広域ネットワークWAN、都市圏ネットワークMANまたはインターネットの一つまたは複数の部分またはこれらのうちの二つ以上の組み合わせと通信してもよい。これらのうち一つまたは複数のネットワークの一つまたは複数の部分は有線または無線であってもよい。一例として、コンピュータシステム1300は無線PANWPANたとえばブルートゥースWPANのような、WIFIネットワーク、WIMAXネットワーク、携帯電話ネットワークたとえばグローバル移動通信システムGSMGlobalSystemforMobileCommunicationsネットワークまたは他の好適な無線ネットワークまたはこれらのうちの二つ以上の組み合わせと通信してもよい。コンピュータシステム1300は、適宜、これらのネットワークのうちの任意のネットワークのために、任意の好適な通信インターフェース1310を含んでいてもよい。通信インターフェース1310は、適宜、一つまたは複数の通信インターフェース1310を含んでいてもよい。本開示は具体的な通信インターフェースを記載および図示するが、本開示は任意の好適な通信インターフェースを考えている。具体的実施形態では、バス1312は、コンピュータシステム1300のコンポーネントを互いと結合するハードウェア、ソフトウェアまたはその両方を含む。一例として、限定するわけではないが、バス1312は、加速グラフィクスポートAGPAcceleratedGraphicsPortまたは他のグラフィクスバス、向上業界標準アーキテクチャEISAEnhancedIndustryStandardArchitectureバス、フロントサイドバスFSBfrontsidebus、ハイパートランスポートHTHYPERTRANSPORT相互接続、業界標準アーキテクチャISAIndustryStandardArchitectureバス、インフィニバンドINFINIBAND相互接続、低ピン数LPClowpincountバス、メモリバス、マイクロチャネルアーキテクチャMCAMicroChannelArchitectureバス、周辺コンポーネント相互接続PCIPeripheralComponentInterconnectバス、PCIエクスプレスPCIXPCIExpressバス、シリアル先進技術アタッチメントSATAserialadvancedtechnologyattachmentバス、ビデオ電子標準協会ローカルVLBVideoElectronicsStandardsAssociationバスまたは他の好適なバスまたはこれらのうち二つ以上の組み合わせを含んでいてもよい。バス1312は適宜一つまたは複数のバスを含んでいてもよい。本開示は具体的なバスを記載および図示しているが、本開示は任意の好適なバスまたは相互接続を考えている。本稿において、コンピュータ可読記憶媒体への言及は、構造を有する一つまたは複数の非一時的な有形のコンピュータ可読記憶媒体を包含する。一例として、限定するわけではないが、コンピュータ可読記憶媒体は、適宜、半導体ベースのまたは他の集積回路ICたとえば、現場プログラム可能なゲートアレイFPGAfieldprogrammablegatearrayまたは特定用途向けICASICapplicationspecificIC、ハードディスク、HDD、ハイブリッドハードドライブHHD、光ディスク、光ディスクドライブODD、光磁気ディスク、光磁気ドライブ、フロッピーディスク、フロッピーディスクドライブFDD、磁気テープ、ホログラフィー記憶媒体、固体式ドライブSSDsolidstatedrive、RAMドライブ、セキュアデジタルSECUREDIGITALカード、セキュアデジタルSECUREDIGITALドライブまたは他の好適なコンピュータ可読記憶媒体またはこれらのうちの二つ以上の組み合わせを含んでいてもよい。本稿では、コンピュータ可読記憶媒体への言及は、特許法のもとでの特許保護の資格のない媒体は除外する。本稿では、コンピュータ可読記憶媒体への言及は、信号伝達の一時的な形伝搬する電気または電磁信号自身のようなは、それが特許法のもとでの特許保護の対象でない限りにおいて、除外する。本開示は、任意の好適な記憶装置を実装する一つまたは複数のコンピュータ可読記憶媒体を考えている。具体的実施形態では、コンピュータ可読記憶媒体は、適宜、プロセッサ1302の一つまたは複数の部分たとえば一つまたは複数の内部レジスタまたはキャッシュのような、メモリ1304の一つまたは複数の部分、記憶装置1306の一つまたは複数の部分またはこれらの組み合わせを実装する。具体的実施形態では、コンピュータ可読記憶媒体はRAMまたはROMを実装する。具体的実施形態では、コンピュータ可読記憶媒体は揮発性または持続性メモリを実装する。具体的実施形態では、一つまたは複数のコンピュータ可読記憶媒体がソフトウェアを具現する。本稿において、ソフトウェアへの言及は、適宜、一つまたは複数のアプリケーション、バイトコード、一つまたは複数のコンピュータプログラム、一つまたは複数の実行形式、一つまたは複数の命令、論理、機械コード、一つまたは複数のスクリプトを包含し、逆もまたしかりである。具体的実施形態では、ソフトウェアは一つまたは複数のアプリケーションプログラミングインターフェースAPIを含む。本開示は、任意の好適なプログラミング言語またはプログラミング言語の組み合わせで書かれたまたは他の仕方で表現された任意の好適なソフトウェアを考えている。具体的実施形態では、ソフトウェアはソースコードまたはオブジェクトコードとして表現される。具体的実施形態では、ソフトウェアはたとえばC、Perlまたはそれらの好適な拡張のような高レベルプログラミング言語で表現される。具体的実施形態では、ソフトウェアは、アセンブリ言語または機械コードのような低レベルプログラミング言語で表現される。具体的実施形態では、ソフトウェアはジャバで表現される。具体的実施形態では、ソフトウェアはハイパーテキストマークアップ言語HTML、拡張可能マークアップ言語XMLまたは他の好適なマークアップ言語で表現される。本開示は、当業者が把握するような本稿に記載される例示的実施形態へのあらゆる変更、置換、変形、改変および修正を包含する。同様に、適切であれば、付属の請求項は、当業者が把握するような本稿に記載される例示的実施形態へのあらゆる変更、置換、変形、改変および修正を包含する。以上の実施例を含む実施形態に関し、さらに以下の付記を開示する。付記1一つまたは複数のコンピューティングデバイスによって:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定のものに適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、段階と;前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを含む、方法。付記2付記1記載の方法であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、方法。付記3付記1記載の方法であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、方法。付記4付記3記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、方法。付記5付記1記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが:前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、方法。付記6付記1記載の方法であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、方法。付記7付記6記載の方法であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、方法。付記8付記7記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。付記9付記7記載の方法であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。付記10一つまたは複数のプロセッサによって実行可能な命令を有するメモリと;前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の数値制約条件は前記数値変数のうちの特定のものに適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、段階と;前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを実行するよう動作可能である、システム。付記11付記10記載のシステムであって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、システム。付記12付記10記載のシステムであって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、システム。付記13付記12記載のシステムであって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、システム。付記14付記10記載のシステムであって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが:前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、システム。付記15付記10記載のシステムであって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、システム。付記16付記15記載のシステムであって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、システム。付記17付記16記載のシステムであって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、システム。付記18付記16記載のシステムであって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、システム。付記19ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティングデバイスによって実行されたときに:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定のものに適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、段階と;前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを実行するよう動作可能である、媒体。付記20付記19記載の媒体であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、媒体。付記21付記19記載の媒体であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、媒体。付記22付記21記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、媒体。付記23付記19記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが:前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、媒体。付記24付記19記載の媒体であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、媒体。付記25付記24記載の媒体であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、媒体。付記26付記25記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。付記27付記25記載の媒体であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。付記28ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定のものに適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、手段と;前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する手段と;前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する手段と;前記第一および第二の数値制約条件のそれぞれを式で表現する手段と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う手段とを含む、システム。付記1′一つまたは複数のコンピューティングデバイスによって:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを含む、方法。付記2′付記1′記載の方法であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、方法。付記3′付記1′または2′記載の方法であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、方法。付記4′付記3′記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、方法。付記5′付記1′ないし4′のうちいずれか一項記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが:前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、方法。付記6′付記1′ないし5′のうちいずれか一項記載の方法であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、方法。付記7′付記6′記載の方法であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、方法。付記8′付記7′記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。付記9′付記7′記載の方法であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。付記10′一つまたは複数のプロセッサによって実行可能な命令を有するメモリと;前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作する、システム。付記11′ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティングデバイスによって実行されたときに:ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、段階と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と;前記第一および第二の数値制約条件のそれぞれを式で表現する段階と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作可能である、媒体。付記12′付記11′記載の媒体であって:前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み;前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み;前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの仕様に基づいて決定され;前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェアモジュールの記号的実行を行うことによって決定される、媒体。付記13′付記11′または12′記載の媒体であって:前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され;前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、媒体。付記14′付記13′記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェアモジュールを実装するプログラミング言語の仕様および前記ソフトウェアモジュールが実行される実行時環境に基づいて推定される、媒体。付記15′付記11′ないし14′のうちいずれか一項記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが:前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い;解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、媒体。付記16′付記11′ないし15′のうちいずれか一項記載の媒体であって:前記ソフトウェアモジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し;前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており;前記ソフトウェアモジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェアモジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、媒体。付記17′付記16′記載の媒体であって:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数は、前記ソフトウェアモジュールの一つまたは複数の入力変数および前記ソフトウェアモジュールの一つまたは複数の出力変数を含み、前記ソフトウェアモジュールに関連付けられた前記要件が、前記ソフトウェアモジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェアモジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェアモジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェアモジュールを対応する実行経路の終わりに到達させるものである、段階と;前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と;前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と;前記事後条件制約条件のそれぞれを否定にする段階と;前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と;制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と;制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェアモジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、媒体。付記18′付記17′記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。付記19′付記17′記載の媒体であって、前記ソフトウェアモジュールに関連付けられた要件に関して前記ソフトウェアモジュールを検証することが:前記ソフトウェアモジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。付記20′ソフトウェアモジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、前記ソフトウェアモジュールは:一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され;前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、手段と;前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する手段と;前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する手段と;前記第一および第二の数値制約条件のそれぞれを式で表現する手段と;前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と;前記ソフトウェアモジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェアモジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う手段とを含む、システム。