"1以上のコンピュータ装置により、ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、を含むことを特徴とする方法。前記1以上の数値の変数は、1以上の入力の数値の変数と1以上の中間の数値の変数とを含み、前記1以上の文字列の変数は、1以上の入力の文字列の変数と1以上の中間の文字列の変数とを含み、前記1以上の入力の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の入力の文字列の変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの仕様に基づいて決定され、前記1以上の中間の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の中間の文字列に変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの記号的実行を行うことで決定される、請求項1記載の方法。前記第二の数値に関する制約は、前記第一の文字列に関する制約と前記第二の演算とに基づいて推定され、前記第二の文字列に関する制約は、前記第一の数値に関する制約と前記第一の演算とに基づいて推定される、請求項1記載の方法。前記第二の数値に関する制約と前記第二の文字列に関する制約は、ソフトウェアモジュールを実現するプログラミング言語と、前記ソフトウェアモジュールが実行されるランタイム環境との仕様に基づいて更に推定される、請求項3記載の方法。全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満たす解を発見することを試みるステップは、前記1以上の数値の変数と前記1以上の文字列の変数とについて異なる可能性のある値を繰返し試み、ある解が発見されるか、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とが満たされないと判定されるか、又はある繰り返し回数が閾値に到達するまで、前記異なる可能性のある値が前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約の全てを満たす解を生成するかを検査するステップと、前記解が発見された場合、前記1以上の数値の変数と前記1以上の文字列の変数の値を出力するステップと、を含む請求項1記載の方法。前記ソフトウェアモジュールは、1以上の条件分岐点と前記1以上の条件分岐点から得られる前記1以上の実行経路とを含み、前記1以上の条件分岐点のそれぞれは、前記1以上の数値の変数と前記1以上の文字列の変数とにより特定される分岐条件に関連され、前記ソフトウェアモジュールの実行の間、前記1以上の条件分岐点のそれぞれで、前記ソフトウェアモジュールは、前記1以上の条件分岐点に関連する分岐条件が満たされるかに依存して、前記1以上の実行経路のうちの実行経路に進む、請求項1記載の方法。前記可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、前記ソフトウェアモジュールの前記1以上の数値の変数と前記1以上の文字列の変数のうちの特定の変数に適用される1以上の制約のセットを決定するステップと、それぞれの制約のセットは、前記ソフトウェアモジュールの前記1以上の実行経路のうちの特定の実行経路に対応し、前記制約が満たされた場合、前記ソフトウェアモジュールに対応する実行経路の終わりに到達させ、前記それぞれの制約のセットを満たす1以上の解を発見するステップと、前記解に基づいて前記ソフトウェアモジュールについて1以上のテスト入力値のセットを生成するステップと、それぞれのテスト入力値のセットを前記ソフトウェアモジュールに適用することで、増加されるテスト範囲で前記ソフトウェアモジュールを検査するステップと、を含む請求項6記載の方法。前記それぞれの制約のセットは、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とに基づいて決定される、請求項7記載の方法。前記可能性のある値について前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールに記号的実行を行い、制約のセットを取得するステップを更に含む、請求項7記載の方法。1以上のプロセッサにより実行可能な命令を含むメモリと、前記メモリに結合され、前記命令を実行する1以上のプロセッサとを備えるシステムであって、前記1以上のプロセッサは、前記命令を実行したときに、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうちの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を有するソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、実行することを特徴とするシステム。前記1以上の数値の変数は、1以上の入力の数値の変数と1以上の中間の数値の変数とを含み、前記1以上の文字列の変数は、1以上の入力の文字列の変数と1以上の中間の文字列の変数とを含み、前記1以上の入力の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の入力の文字列の変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの仕様に基づいて決定され、前記1以上の中間の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の中間の文字列に変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの記号的実行を行うことで決定される、請求項10記載のシステム。前記第二の数値に関する制約は、前記第一の文字列に関する制約と前記第二の演算とに基づいて推定され、前記第二の文字列に関する制約は、前記第一の数値に関する制約と前記第一の演算とに基づいて推定される、請求項10記載のシステム。前記第二の数値に関する制約と前記第二の文字列に関する制約は、ソフトウェアモジュールを実現するプログラミング言語と、前記ソフトウェアモジュールが実行されるランタイム環境との仕様に基づいて更に推定される、請求項12記載のシステム。全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満たす解を発見することを試みるステップは、前記1以上の数値の変数と前記1以上の文字列の変数とについて異なる可能性のある値を繰返し試み、ある解が発見されるか、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とが満たされないと判定されるか、又はある繰り返し回数が閾値に到達するまで、前記異なる可能性のある値が前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約の全てを満たす解を生成するかを検査するステップと、前記解が発見された場合、前記1以上の数値の変数と前記1以上の文字列の変数の値を出力するステップと、を含む請求項10記載のシステム。前記ソフトウェアモジュールは、1以上の条件分岐点と前記1以上の条件分岐点から得られる前記1以上の実行経路とを含み、前記1以上の条件分岐点のそれぞれは、前記1以上の数値の変数と前記1以上の文字列の変数とにより特定される分岐条件に関連され、前記ソフトウェアモジュールの実行の間、前記1以上の条件分岐点のそれぞれで、前記ソフトウェアモジュールは、前記1以上の条件分岐点に関連する分岐条件が満たされるかに依存して、前記1以上の実行経路のうちの実行経路に進む、請求項10記載のシステム。前記可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールの前記1以上の数値の変数と前記1以上の文字列の変数のうちの特定の変数に適用される1以上の制約のセットを決定するステップと、それぞれの制約のセットは、前記ソフトウェアモジュールの前記1以上の実行経路のうちの特定の実行経路に対応し、前記制約が満たされた場合、前記ソフトウェアモジュールに、対応する実行経路の終わりに到達させ、前記それぞれの制約のセットを満たす1以上の解を発見するステップと、前記解に基づいて前記ソフトウェアモジュールについて1以上のテスト入力値のセットを生成するステップと、それぞれのテスト入力値のセットを前記ソフトウェアモジュールに適用することで、増加されるテスト範囲で前記ソフトウェアモジュールを検査するステップと、を含む請求項15記載のシステム。前記それぞれの制約のセットは、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とに基づいて決定される、請求項16記載のシステム。前記可能性のある値について前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールに記号的実行を行い、制約のセットを取得するステップを更に含む、請求項16記載のシステム。1以上のコンピュータ装置に、ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、を実行させる命令を含むプログラムを記録したコンピュータ読み取り可能な記録媒体。ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析する手段と、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定する手段と、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定する手段と、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現する手段と、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現する手段と、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査する手段と、を備えることを特徴とするシステム。本発明の開示は、添付図面に例示される幾つかの実施の形態を参照して詳細に記載される。以下の記載では、本発明の開示の全体的な理解を提供するため、多数の特定の詳細が述べられる。しかし、本発明の開示は、これらの特定の詳細の一部又は全部なしに実施される場合があることは、当業者にとって明らかである。他の例では、公知のプロセスのステップ及び/又は構造は、本発明を不必要に不明瞭にしないように詳細に説明されていない。さらに、本発明の開示は特定の実施の形態と合わせて記載されるが、本発明の記載は、記載される実施の形態の本発明を制限することが意図されないことを理解されたい。それとは反対に、本発明の記載は、特許請求の範囲により定義される本発明の開示の精神及び範囲に含まれる場合があるような代替、変更及び等価な概念をカバーすることが意図される。ソフトウェアアプリケーションは、多数のソフトウェアモジュールに編成されることがあり、それぞれのソフトウェアモジュールは、特定の機能を実行するコードを含む場合がある。典型的なシナリオでは、ソフトウェアモジュールは、任意の数の入力変数又は出力変数を有する場合がある。ソフトウェアモジュールが起動されたとき、実際の入力値は、ソフトウェアモジュールの入力変数に割り当てられた値として、たとえばソフトウェアモジュールを起動するコードによりソフトウェアモジュールに通過される場合がある。ソフトウェアモジュールのコードは、実際の入力値に関連して実行される場合がある。最終的に、ソフトウェアモジュールの出力変数の実際の出力値は、ソフトウェアモジュールにより決定されリターンされる場合があり、その時点で、ソフトウェアモジュールは、その実行を完了する。さらに、ソフトウェアモジュールのコードにより決定される実際の出力値は、通常、その起動に応じてソフトウェアモジュールに通過された実際の入力値に依存する。さらに、ソフトウェアモジュールは、中間変数とも呼ばれる任意の数のローカル変数を有し、その値は、直接的又は間接的に、入力変数の値に依存する場合がある。ローカル変数は、ローカルスコープを有する。ローカル変数は、ローカル変数が宣言されたソフトウェアモジュールのコンテキストにおいて存在し、ローカル変数が宣言されたソフトウェアモジュールのコンテキストのみからアクセス可能である。対照的に、ソフトウェアモジュールが属するソフトウェアアプリケーションは、任意の数のグローバル変数を有する場合がある。グローバル変数は、ソフトウェアアプリケーション自身においてグローバルスコープを有し、ソフトウェアアプリケーションに属する全てのソフトウェアモジュールにアクセス可能である。ソフトウェアアプリケーションが起動されたとき、ソフトウェアアプリケーションは、グローバル変数の値をアクセス又は変更する場合があり、値の変更は、ソフトウェアモジュールがその実行を完了した後でさえ持続する。特定の実施の形態では、第一の変数の値が第二の変数の値に基づいて決定されたときすなわち第一の変数の値は第二の変数の値に依存する、第一の変数は、第二の変数に依存すると考えられる。ある変数は、入力であろうと出力であろうと、ローカルであろうとグローバルであろうと、たとえば限定されることなしに、文字、文字列、整数、浮動小数、倍精度浮動小数点数、ブール、ポインタ、アレイ及びエミュレーションのような特定のデータタイプを有する。ある変数のデータタイプは、どのようなタイプのデータたとえば実際の値が変数に割り当てられる場合があるかを示す。たとえば、整数値のみがそのタイプが整数である変数に割り当てられるべきであり、真偽値のみが、そのタイプがブールである変数に割り当てられるべきである。異なるプログラム言語は、特定のデータタイプに適用される場合がある異なる動作と同様に、特定の言語で書かれたソフトウェアモジュール又はアプリケーションが有する場合がある異なるデータタイプを定義する場合がある。特定の実施の形態では、プログラミング言語は、データタイプは、文字列と数値といった2つのカテゴリに分割される場合がある。数値データのタイプは、たとえば限定されるものではないが、整数、浮動小数点数、整数、倍精度浮動小数点数、及びブールのような文字列でないデータタイプを含む場合がある。文字列は、異なるプログラミング言語がタイプ文字列stringを異なって定義する場合があるが、多くのプログラミング言語において利用可能なデータタイプである。たとえば、Javaプログラミング言語は、文字の不変のアレイとして文字列を表すJavaクラスjavalangStringとしてタイプ文字列stringを定義するものである。この場合、ひとたび文字列変数が宣言されて形成されると、その値は、その後に変化することができない。ある文字列の変数の値への変更は、宣言及び構築されている新たな文字列の変数となる。また、javalangStringは、ある文字列の変数に適用される場合があるメソッドmethodと呼ばれる多くの演算を提供する。他方で、Cプログラミング言語により、ある文字列は、ヌル文字で終端される1次元の文字配列として定義される。あるC文字列は、その値がインプレースで変更される場合があるように、変更可能である。実際に、配列におけるそれぞれの文字は、個々に変更される場合がある。それぞれのプログラム言語は、利用可能な特定の数値データのタイプが言語から言語に変化する場合があるが、幾つかの数値データのタイプを一般的に定義する。整数、浮動小数点数、倍精度浮動小数点数及びブールは、大部分のプログラミング言語により一般的に定義される数値データのタイプである。さらに、異なるプログラミング言語は、特定の数値データのタイプを異なって定義する場合がある。たとえば、Javaプログラミング言語は、プリミティブなデータのタイプintとして又はJavaクラスjavalangIntegerとして特定の数値データのタイプを異なって定義する場合がある。クラスjavalangIntegerは、整数の変数に適用される動作すなわちメソッドを提供する。他方で、Cは、異なるデータのサイズを有する整数の変数を宣言するために使用される場合があるshort、int及びlongといった3つのプリミティブなデータのタイプを提供する。あるソフトウェアモジュールの入力、出力又はローカル変数に課される任意の数の制約が存在する。特定の実施の形態では、変数に課される制約は、たとえば限定されるものではないが、どのような値がその変数に割り当てられるか、変数に割り当てられるデータ値のサイズ、又は変数に課される他の適用可能な条件又は制限を指定する場合がある。係る変数の制約は、ソフトウェアモジュールの設計仕様又は形式的な要件、ソフトウェアモジュールを実現するために使用されるプログラミング言語の仕様、ソフトウェアモジュールのプログラムロジックに含まれるコード、ソフトウェアモジュールが実行されるランタイム環境、又は他の適用可能な要素から特定される場合がある。たとえば、制約は、整数の変数aのみが0xFFFFFFFF以下である整数値に割り当てられることを指定する整数値aに課される。これは、ソフトウェアモジュールは、4バイトを使用したそれぞれの整数を表すランタイム環境で実行されるからである。整数の変数aに課される制約は、式a<0xFFFFFFFFとして表される場合がある。別の例として、制約は、文字列の変数sの長さすなわち文字数が8でなければならないことを指定する文字列変数sに課される場合がある。この場合、文字列の変数sに課される制約は、例としてJavaプログラミング言語のシンタックスを使用して、別の式slength8として表される場合がある。あるソフトウェアモジュールの1つの変数に課される制約は、直接的に又は間接的に、ソフトウェアモジュールの別の変数の値に課される制約に依存する場合がある。たとえば、1整数の変数bが10以上である整数の値にのみ割り当てられる、及び2整数の変数bが変数aの値未満である整数の値にのみ割り当てられる、ことを指定する2つの制約が、整数の変数bに一緒に課される場合がある。この場合、一緒に整数の変数bに課される2つの制約は、として表される場合があり、それぞれの制約は、この別の式として表される。特定の実施の形態では、あるソフトウェアモジュールは、任意の数の数値又は文字列の変数を有する場合があり、これらの変数は、ソフトウェアモジュールの入力変数又はローカル変数すなわち中間変数である場合がある。特定の実施の形態では、ある制約のセットは、ソフトウェアモジュールの特定の数値又は文字列の変数に課される場合がある。なお、ある制約のセットが、あるソフトウェアモジュールのありとあらゆる変数に課される必要はない。特定の実施の形態では、数値の変数が与えられた場合、任意の数の数値の制約又は文字列の制約を有する場合がある。たとえば、整数の変数bは、その値が10以上でなければならないことを指定する数値の制約たとえば制約b10を有する場合がある。整数の変数bは、その値のテキストすなわち文字列の表現は文字列182に等しくなければならないことを指定する文字列の制約たとえば制約btoString182を有する場合もある。この場合、整数の変数bに課される制約のセットは、数値の制約と文字列の制約の両者、従って制約が混成されたセットであるたとえば182を含む。同様に、特定の実施の形態では、文字列の変数が与えられると、任意の数の文字列の制約又は数値の制約を有する場合がある。たとえば、文字列の変数sがその値がサブの文字列caで開始しなければならないことを指定する文字列の制約たとえば制約ssubstringca又はsstartsWithを有する場合がある。文字列の変数sは、その値が8の文字の長さを有しなければならないことを指定する数値の制約たとえば制約slength8を有する場合もある。この場合、文字列の変数sに課される制約のセットは、数値の制約と文字列の制約の両者、従って制約が混成されたセットであるたとえばca8を含む。特定の実施の形態では、あるソフトウェアモジュールに課される制約は、入力、出力及びローカル変数を含めて、その変数に課される全ての制約を組み合わせて含む場合がある。たとえば、整数の変数bと文字列の変数sの両者があるソフトウェアモジュールmに属するとする。この場合、ソフトウェアモジュールm自身に課される制約のセットは、変数b及びsのそれぞれに課される2つの制約のセットの論理結合を含み、これは、182ca8に等しい。これも、数値の制約と文字列の制約の両者を含むために、制約が混成されたセットである。特定の実施の形態では、任意の数の数値の変数又は文字列の変数を有するソフトウェアモジュールに課される制約が混成されたセットを決定及び解決するために有益である。また、あるソフトウェアモジュールの特定の変数に課される制約が混成されたセットを決定及び解決するために有益である。特定の実施の形態では、制約のセットを解決することは、そのセットに含まれる全ての制約を満足する1以上の解を発見するのを試みることを意味する。図1は、あるソフトウェアモジュール又はあるソフトウェアモジュールのある変数に課される制約を決定及び解決する例示的な方法を示す。図2は、あるソフトウェアモジュール又はあるソフトウェアモジュールの変数に課される制約を決定及び解決する例示的なシステム200を示す。特定の実施の形態では、図2に示されるシステム200の構成要素は、コンピュータハードウェア又はソフトウェア或いはその組み合わせとして実現される。図1及び図2は、互いに関連して記載される。特定の実施の形態では、あるソフトウェアモジュールは、任意の数の数値の変数又は文字列の変数を有する場合がある。たとえばソフトウェアモジュールmは、整数の変数vi、ブール変数vb及び文字列の変数vsを有する場合がある。この場合、変数vi及びvbは、数値の変数である。特定の実施の形態では、これらの変数は、ソフトウェアモジュールの入力、出力又はローカル変数である場合がある。特定の実施の形態では、はじめに、ソフトウェアモジュールの特定の数値の変数に課される任意の数の数値の制約、及びソフトウェアモジュールの特定の文字列の制約に課される任意の数の文字列の制約が存在する場合がある。より詳細には、数値の制約のセットが、特定の数値の変数について指定されて、特定の数値の変数に課されるか、又は、文字列の制約のセットが、特定の文字列の変数について指定されて、特定の文字列の変数に課される場合がある。それぞれの制約のセットは、1以上の特定の制約を含む場合がある。たとえば、数値の制約のセットnc1viが、整数の変数viについて指定され、整数の変数viに課され、数値の制約のセットnc1vbが、ブール変数vbについて指定され、ブール変数vbに課され、文字列の制約のセットsc1vsが、文字列の変数vsについて指定され、文字列の変数vsに課される。特定の実施の形態では、これらの制約の最初のセットたとえばnc1vi、nc1vb及びsc1vsが、ソフトウェアモジュールの設計仕様又は形式的な要件に基づいて指定される。特定の実施の形態では、ソフトウェアモジュールにおいて、ソフトウェアモジュールの特定の数値の変数に適用される任意の数の演算が存在し、この演算は、数値の入力を必要とするか、又は数値の出力を生成する。たとえば、整数の変数viに適用される演算は、rivi10であり、この演算は、入力としてvi及び10の値である2つの数値を要し、出力としてriの値である数値を生成する。特定の実施の形態では、ソフトウェアモジュールにおいて、ソフトウェアモジュールの特定の数値の変数に適用される任意の数の動作が存在し、この演算は、文字列の入力を要するか又は文字列の出力を生成する。たとえば、ブール変数vbに適用される演算は、vbtoStringであり、この演算は、その出力として、ブールの変数vbの値の文字列の表現たとえば文字列trueである、文字列の値を生成する。特定の実施の形態では、ソフトウェアモジュールにおいて、ソフトウェアモジュールの特定の文字列の変数に適用される任意の数の演算が存在し、この演算は、文字列の入力を要するか又は文字列の出力を生成する。たとえば、文字列の変数vsに適用される演算は、rsvscontactであり、この演算は、入力としてvs及びabcの値である2つの文字列の値を要し、出力としてrsの値である文字列の値を生成する。特定の実施の形態では、ソフトウェアモジュールにおいて、ソフトウェアモジュールの特定の文字列の変数に適用される任意の数の演算が存在し、この演算は、数値の入力を要するか又は数値の出力を生成する。たとえば、文字列の変数vsに適用される演算は、vslengthであり、この演算は、文字列の変数vsの値に含まれる文字数を示す数値をその出力として生成する。文字列の変数vsに適用される別の演算は、vssubstringであり、この演算は、入力として2つの数値を要する。特定の実施の形態は、図1のステップ102に示されるように、たとえばソフトウェアモジュールmといったソフトウェアモジュール、ソフトウェアモジュールのたとえば整数の変数viに課される数値の制約nc1vi及びブール変数vbに課される数値の制約nc1vbといった特定の数値の変数について最初に指定され、課される数値の制約のセット、及び、ソフトウェアモジュールのたとえば文字列の変数vsに課される文字列の制約sc1vsといった特定の文字列の変数について最初に指定され、課される文字列の制約のセットを分析する。特定の実施の形態では、数値及び文字列の制約は、ソフトウェアモジュールの入力又は中間の変数すなわちローカル変数の何れかに課される。勿論、特定の実施の形態では、数値の制約のセットがソフトウェアモジュールのありとあらゆる数値の変数に最初に課される必要はなく、また、文字列の制約のセットがソフトウェアモジュールのありとあらゆる文字列の変数に最初に課される必要はない。特定の数値の変数のみが関連される数値の制約を最初に有し、また、特定の文字列の変数のみが関連される文字列の制約を最初に有することもできる。特定の実施の形態では、ソフトウェアモジュールの入力変数に最初に課される数値又は文字列の制約について、ソフトウェアモジュールの設計仕様又は形式的な要件に従って制約が決定される場合がある。ソフトウェアモジュールの中間の変数に最初に課される数値又は文字列の制約について、ソフトウェアモジュールで記号的実行を行うことで制約が決定される場合がある。記号的実行は、図8と共に以下に詳細に記載される。要するに、特定の実施の形態は、ソフトウェアモジュールの入力変数のそれぞれに記号の値を割り当てる一方で、ソフトウェアモジュールでの記号的実行を行う。ソフトウェアモジュールの中間の変数は、直接的又は間接的に、ソフトウェアモジュールの1以上の入力変数に依存するので、ソフトウェアモジュールで記号的実行を行うことで、中間変数について、それが特定の入力変数に有する依存度を示す記号の表現のセットが得られる。特定の実施の形態は、中間の変数について得られる記号的表現のセットに基づいて中間の変数に課される制約と、中間の変数が依存する特定の入力の変数に課される制約のセットを決定する。たとえば、ソフトウェアモジュールmにより、viは入力変数、riは中間変数、及びrivi10とする。この場合、ソフトウェアモジュールmに記号的実行を行うことで、中間の変数riが入力の変数viに依存することを判定する。さらに、vi0であるように、数値の制約が入力の変数viに課されているとする。記号的実行の結果と入力の変数viに課された数値の制約とに基づいて、数値の制約は、ri10となるように中間変数riについて決定される。図1のステップ102に示される分析から、特定の実施の形態は、図1のステップ104に示されるように、ソフトウェアモジュールの特定の数値の変数に課された文字列の制約のセット、及びソフトウェアモジュールの特定の文字列の制約に課された数値の制約のセットを推定する。特定の実施の形態では、図1のステップ102及び104は、図2に示されるシステム200の構成要素202により実行される場合がある。特定の実施の形態では、構成要素202は、ソフトウェアモジュール212及びソフトウェアモジュール212の変数に最初に課された制約214を入力として受け、この制約は、ソフトウェアモジュールの数値の変数について最初に指定され、課された数値の制約と、ソフトウェアモジュールの文字列の変数について最初に指定され、課された文字列の制約を含む。構成要素202は、適用可能な分析を行い、ソフトウェアモジュール212の数値の変数に課された文字列の制約と、ソフトウェアモジュール212の文字列の変数に課された数値の制約とを推定する。構成要素202は、出力として、ソフトウェアモジュール212の変数に課された指定された制約であって、推定された制約の両者含む数値の制約と文字列の制約とが混成されたセットを提供する。特定の実施の形態では、ソフトウェアモジュールの変数の制約は、様々な要素に基づいて推定される場合があり、本発明の開示は、適用可能な要素を含んでいる。たとえば限定することなしに、特定の変数に適用される演算、ソフトウェアモジュールを実現するために使用されるプログラミング言語の仕様、ソフトウェアモジュールが実行されるランタイム環境及びこれらの複数の要素の組み合わせに基づいて、数値の制約は、数値の変数と文字列の変数との両者について推定され、文字列の制約は、数値の変数と文字列の変数の両者について推定される。特定の実施の形態では、数値の変数が与えられると、数値の変数に適用される演算に基づいて文字列の制約が推定され、これにより、文字列の結果が生成される。たとえば、splitという2つの演算がソフトウェアモジュールmにおける整数の変数viに適用されるとする。この演算の最初の手順は、整数の変数viの値の文字列の表現たとえば数182は、文字列182として表現されるを生成し、次の手順で、この文字列を文字0の位置で新たな文字列に分割する。第二の演算すなわち文字列の分割演算を成功させるためたとえばヌル文字列とならないため、整数の変数viの値の文字列の表現が少なくとも1つの文字0を含まなければならないという、文字列の制約が演算から推定される。特定の実施の形態では、数値の変数が与えられると、数値の制約は、数値の変数に適用される演算に基づいて推定され、これにより数値の結果が生成される。たとえば、Mathsqrtという演算がソフトウェアモジュールmにおける整数の変数viに適用されるとする。この演算は、整数の変数viの値の平方根を与える。この演算をエラーに遭遇することなしに実行するため、整数の変数viの値が0以上でなければならないことを指定する数値の制約が演算から推定される。特定の実施の形態では、文字列の変数が与えられると、文字列の変数に適用される演算に基づいて文字列の制約が推定され、これにより文字列の結果が生成される。たとえば、srepalceAllという演算がソフトウェアモジュールmにおける文字列の変数sに適用されるとする。この演算は、文字列の変数sで発見される全てのサブ文字列abcをxyzで置き換える。この演算が文字列の変数sの値に実際の影響を及ぼすため、文字列の変数sの値が少なくとも1つのサブ文字列abcの発生を含まなければならないという、文字列の制約が演算から推定される。特定の実施の形態では、文字列の変数が与えられると、数値の制約は、数値の結果を生成することになる文字列の変数に適用される演算に基づいて推定されるか、1以上の数値の入力を受けることになる文字列の変数に適用される演算に基づいて推定される。たとえば、sstartsWithという演算がソフトウェアモジュールmにおける文字列の変数sに適用され、この演算は、文字列の変数sの値がサブ文字列abcで開始するかを示す真又は偽としてブールの結果を生成する。この演算を上手く実行するため、文字列の変数sの値は、少なくとも3つの文字を有さなければならない。従って、文字列の変数sの長さが3以上でなければならないことを指定する数値の制約がこの演算から推定される。別の例として、ssubstringという演算がソフトウェアモジュールmにおける文字列の変数mに適用されるとする。この演算は、入力として数値を受ける。この演算を上手く実行するためたとえばヌル文字列とならないため、文字列の変数sの値は、少なくとも6つの文字を有さなければならない。従って、文字列の変数sの長さが6以上でなければならないことを指定する数値の制約がこの演算から推定される。先の例では、ソフトウェアモジュールにおいて、文字列の結果を生成する演算が数値の変数に適用されるか、又は、数値の入力を受けるか又は数値の結果を生成する演算が文字列の変数に適用される。特定の実施の形態では、これらの演算から、数値の制約が推定されて、特定の文字列の変数に課され、文字列の制約が推定されて、特定の数値の変数に課される。特定の実施の形態では、数値又は文字列である変数が与えられると、変数に課される完全な制約のセットは、もしあれば変数について最初に指定された制約と、もしあれば変数について推定される制約との両者を含む。この制約のセットは、数値の制約又は文字列の制約、或いはその両者を含む。変数に課される制約のセットは、変数に適用される個々の演算に基づいて変数について推定されるため、特定の実施の形態は、このように取得された制約のセットを相互作用するハイブリッドな制約のセットと呼ぶ。特定の実施の形態では、任意の数の数値又は文字列の変数を有するソフトウェアモジュールが与えられると、ソフトウェアモジュール自身に課される制約のセットは、ソフトウェアモジュールの個々の変数に課される全ての制約を含む。あるソフトウェアモジュールの変数に課されるハイブリッドな制約のセットが与えられると、特定の実施の形態は、図1のステップ106に示されるように、数式たとえばvi0,vbtrue又はslength6でセットにおけるそれぞれの数値の制約を表し、セットにおけるそれぞれの文字列の制約を有限状態マシンFSMで表す。一般に、FSMは、有限の状態、これら状態間の遷移及びアクションの数から構成される挙動のモデルである。特定の実施の形態では、FSMは、文字列を表現するために使用される。図3は、文字列を表現するために使用される幾つかのFSMを示す。図3において、それぞれのFSMにより、中間の状態は、1つの円により表現され、許可状態は、二重の円により表現され、ある状態への入力は、円につながる矢印により表現される。たとえば、FSM310は、ある文字列sを表し、この文字列は、任意の文字を有し、任意の長さからなる。FSM320は、ある文字列を表し、この文字列は、少なくとも1つの文字を有しており、文字列の最後の文字は、Zであり、制約SendsWidthtrueを表現するために使用される。FSM330は、ある文字列を表し、この文字列は、3以上の文字を有しており、Slength3を表現するために使用される。FSM340は、ある文字列Sを表し、この文字列は、少なくとも1つの文字を有し、少なくとも1つのZを含み、Zの遷移は、文字列における最後のZを意味する。FSM350は、文字列Sを表し、この文字列は、Zである任意の文字を有さない。制約を考える。この制約から、a0である場合に、Zであることを推定することができる。FSM340は、先の制約が満足された場合、すなわち文字列Sが少なくとも1つのZの文字を含み、Sに生じる最後のZは、aの値に等しいインデックスである場合を表す。他方で、FSM350は、制約のセットが満たされない場合、すなわち文字列Sが任意の文字Zを含まない、従ってa1である場合を表す。従って、制約aSlastIndexOfにより、記号的実行ツリーにおける分岐となり、一方のブランチで、更なる数値の制約a0をもつFSM340の場合が想定され、他方のブランチで、更なる制約a1をもつFSM350の場合が想定される。図4は、文字列Sとそのサブ文字列の1つSsubstringを表すために使用される別の例示的なFSM400を示す。この例では、状態402は、文字列Sの開始ポイントであり、状態404は、文字列Sの許可状態すなわち終了ポイントである。サブ文字列Ssubstringは、第3の文字で開始し、第五の文字で終了するSのサブ文字列である。なお、Javaプログラミング言語によれば、インデックスは、0で開始し、すなわち最初のエレメントのインデックス番号は、0である。従って、インデックス番号2は、第三のエレメントを示し、インデックス番号4は、第五のエレメントを示す。サブ文字列Ssubstringについて、開始ポイントは、文字列Sの第三の文字に対応する文字列Sの開始状態402から第三の状態であり、文字列Sの第三の文字に対応する。図4では、3つの状態412A,412B及び412Cが存在し、それぞれの状態は、開始状態402からの第三の状態であり、それらの1つは、サブ文字列Ssubstringについて可能性のある開始状態412である。サブ文字列Ssubstringについて、終了ポイントすなわち許可状態は、文字列Sの開始状態402から第五の状態であり、文字列Sの第五の文字に対応する。図4では、3つの状態414A,414B及び414Cが存在し、これらの状態は、開始状態402から第五の状態である、それらのうちの1つは、サブ文字列Ssubstringについて可能性のある許可状態414である。なお、図4において、εは、ゼロ入力の状態を示す。特定の実施の形態では、制約のセットが与えられると、セットからのそれぞれの数値の制約は、適用可能な数式を使用して表現され、セットからのそれぞれの文字列の制約は、適用可能なFSMを使用して表される。さらに、このように表現された制約のセットが与えられると、特定の実施の形態は、図1のステップ108に示されるように、同時にセットにおける全ての制約を満たす1以上の解を発見するために制約を解くことを試みる。特定の実施の形態では、図1のステップ108は、図2に示されるシステム200の構成要素204により実行される。特定の実施の形態では、構成要素204は、SMTSatisfactoryModuloTheoriesに部分的に基づいて実現される制約の解決手段である。特定の実施の形態では、構成要素204は、数式を使用して表現される数値の制約と、FSMを使用して表現される文字列の制約の一方又は両方を含む制約のセットを入力として受け、セットから全ての制約を満たす1以上の解を発見することを試みる。何れかの解が発見された場合、構成要素204は、その出力として解を与える。勿論、制約のセットがセットからの全ての制約を満たす何れかの解を有さない可能性がある。たとえば、制約のセット0を考える。この場合、s及びqは文字列であり、a及びbは整数である。同時にこのセットからの全ての制約を満たすs、q、a及びbの値の組み合わせは存在しない。従って、この特定の制約のセットは満足されない。特定の実施の形態は、反復アルゴリズムを使用して制約が混成されたセットを解く。特定の実施の形態は、FSMを使用して表現された、セットからの全ての文字列の制約を文字列の領域でグループ化し、数式を使用して表現された、セットからの全ての数値の制約を数値の領域でグループ化する。特定の実施の形態は、次いで、1セットにおける全ての制約を満たす1以上の解が発見されるまで、2セットにおける全ての制約を満たす解がないと判定されるまで、又は3実行される繰返しの回数が予め決定された閾値に到達するまで1~3の何れか早いほう、数値領域又は文字列領域の何れかで1以上の解すなわちセットにおける全ての数値の制約又はセットにおける全ての文字列の制約の何れかを満足させる解を発見する試みを繰返し、一方の領域で発見された解を他方の領域に供給する。特定の実施の形態は、SMTSatisfactoryModuloTheory解法を使用して数値の領域において数値の制約を解き、正規表現ユニオンアルゴリズム、交差アルゴリズム、補完アルゴリズム、Kleenestarアルゴリズム及び他の適用可能なアルゴリズムを使用して、文字列領域において文字列の制約を解く。さらに、特定の実施の形態は、制約が混成されたセットについて1以上の解を発見するのを試みるとき、以下を考慮する。はじめに、数値領域のみにおける数値の制約が満足のいくものではない場合すなわち、セットにおける数値の制約を満たす解が存在しない場合、全体の制約のセットが満足のいくものではない。文字列領域のみにおける文字列の制約の解がヌル文字列すなわち空の文字列である場合、セットにおいて数値の制約が全くない場合、そのセットは満足のいくものではなく、さもなければ、そのセットにおける数値のセットは、ヌル文字列により更に制約される。繰返しの手順を更に説明するため、例示的な制約のセットsstartsWithsendsWith4を考える。この場合、sは文字列であり、a,b,c及びdは整数である。この制約のセットを満たす解は、セットにおける全ての個々の制約が同時に満たす、文字列s及び整数a,b,c及びdのそれぞれについて5つの値の組み合わせが存在することを意味する。より詳細には、制約sstartWithを満足させるため、sの最初の3つの文字はuvwとなる必要がある。制約sendsWithを満たすため、sの最後の3つの文字は、xyzとなる必要がある。制約aslastIndexOfを満たすため、sにおける文字tの最後の発生は、aの値に等しいインデックス番号である。制約slength4を満たすため、a及びdの値の合計は、4以上でなければならない。制約c0を満たすため、cの値は、0よりも大きくなければならない。制約d7であることを意味する。制約aslastIndexOfは、sにおける文字tの最後の発生は、aの値に等しいインデックス番号を有さなければならない。tはsにおける最後の文字ではないので、これは、a3であることを意味する。特定の実施の形態は、sの解から導出される、a、b及びcに課される3つの更なる数値の制約524を、セットからの4つの数値の制約522に追加し、文字列sの解から導出されたものと同様に、セットからのものを含めて、全ての数値の制約522,524を満たすa、b、c及びdの値を発見するのを試みる。さらに、全ての数値の制約を満たす整数a、b、c及びdの多数の値が存在する場合、特定の実施の形態は、最小の値を最初に選択する。セットからの4つのオリジナルの数値の制約522と、3つの更なる導出された数値の制約524とから、特定の実施の形態は、a、b、c及びdについて可能な解をa5、b7、c1及びd1として決定する。実際に、aについて、5,6である2つの可能な値が存在する。値5は、最小であり、従ってaについて最初に選択される。これらの4つの値は、文字列の制約に対して検証されるため、文字列領域510にフィードバックされる。第三の繰返し533の間、第二の繰返し532の間に数値領域520で発見されるa、b、c及びdの解は、文字列領域510において文字列の制約に対して確認される。sがuvwtxyzである場合、tのインデックスは3であり且つaの値に等しいはずであるので、aは5に等しくすることはできない。このaに関する新たな制約526すなわちa5は、数値領域520にフィードバックされる。第四の繰返し534の間、制約526であるa5は、他の既存の数値の制約522,524に追加される。全ての現在存在する数値の制約522,524及び526を満たすa、b、c及びdの次の可能性のある解は、a6、b7、c1及びd1である。この解は、文字列領域510にフィードバックされる。第五の繰返し535の間、前の繰返しの間に数値領域520においてa、b、c及びdについて発見された解すなわち、a6、b7、c1及びd1は、文字列領域510において文字列の制約に対して同様に確認される。さらに、sがuvwtxyzである場合、aを6に等しくすることはできない。これにより、aに関して新たな制約528であるa6が得られ、数値領域520にフィードバックされる。第六の繰返し536の間、制約528であるa6は、他の既存の数値の制約522,524,526に追加される。全ての数値の制約522,524,526,528をい満たす解を発見する試みが行われる。しかし、全ての現在の既存の数値の制約522,524,526及び528を満たすa、b、c及びdの値が存在しない。従って、sがuvwtxyzに等しい場合、全ての数値の制約を満たすa、b、c及びdの発見することができる解が存在しない。なお、この場合、sは7を超える文字を有することはできない。これは、3つの制約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で、CONDITION1が満たされた場合、実行経路は処理ステップ612に進み、CONDITION1が満たされない場合、実行経路は、処理ステップ614に進む。条件分岐点602において入れ子構造にされた条件分岐点604で、CONDITION2が満たされた場合、実行経路は、処理ステップ616に進み、CONDITION2が満たされない場合、実行経路は終了する。条件分岐点602において入れ子構造にされる条件分岐点606で、CONDITION3が満たされた場合、実行経路は終了し、CONDITION3が満たされない場合、実行経路は、条件分岐点608に進む。条件分岐点606において更に入れ子構造にされた条件分岐点608で、CONDITION6が満たされた場合、実行経路は処理ステップ608に進み、CONDITION6が満たされない場合、実行経路は、処理ステップ622に進む。図6において、5つの可能性のある実行経路が存在し、ソフトウェアモジュールは、個々の条件分岐点602,604,606及び608で分岐条件が満たされたかに依存して、5つの可能性のある実行経路の何れか1つに沿って進む。特定の実施の形態は、分岐条件を表す変数に課される数値又は文字列の制約として分岐条件を考える。たとえば、SAMPLECODE1のライン1で、分岐条件はmnknとして表される。この制約のセットを満たすm、n及びkの解により、分岐条件は満たされすなわち、当てはまり、ソフトウェアモジュールに1つの実行経路すなわち、コードのif部分に沿って進行させる。分岐条件が満たされない場合、mの値は、nの値以下であるか、又はkの値は、10よりも大きい。これは、m、n及びkに課される別の制約のセットとして表現される。この第二の制約のセットを満たすm、n及びkの解により、分岐条件が満たされずすなわち、当てはまらず、ソフトウェアモジュールに別の実行経路すなわち、コードのelse部分に沿って進行させる。結果的に、特定の実施の形態は、ソフトウェアモジュールにおけるそれぞれの可能性のある実行経路に対応する制約のセットを決定し、検査の入力として解を使用してソフトウェアモジュールを検査する。図7は、1以上の条件分岐点から得られる複数の可能性のある実行経路を含むソフトウェアモジュールを検査する例示的な方法を示す。特定の実施の形態では、ソフトウェアモジュールは、任意の数の変数たとえば入力又はローカルの変数及び任意の数の条件分岐点たとえば、ifelse命令文を有する。それぞれの条件分岐点は、1以上の変数により指定された分岐条件に関連される。特定の実施の形態では、分岐条件は、任意の数のサブ条件を含む。条件分岐点に関連する分岐条件が満たされるかに依存して、ソフトウェアモジュールは、異なる実行経路に沿って進む。特定の実施の形態は、ソフトウェアモジュールのそれぞれの可能性のある実行経路について、図7のステップ702で示されるように、ソフトウェアモジュールにそれに沿って進行させ、その実行経路の終わりに到達させる記号的表現のセットを決定するため、ソフトウェアモジュールで記号的実行を行う。それぞれの記号的表現のセットを決定するとき、もしあれば、たとえば、図1のステップ104に関連して記載されるようにソフトウェアモジュールの特定の変数について推定される数値及び文字列の制約と同様に、もしあれば、たとえば図1のステップ102に関連して記載されるようにソフトウェアモジュールの特定の変数に最初に課された数値及び文字列の制約を組み入れる。特定の実施の形態では、図7のステップ702は、図2に示されるシステム200の構成要素206により実行され、このシステムは、ソフトウェアモジュール212を入力として受け、ソフトウェアモジュール212で記号的実行を行い、ソフトウェアモジュール212の実行経路に対応する記号的表現の出力のセットを与える。コンピュータ科学の分野では、記号的実行は、抽象解釈の場合として、実際の値ではなく記号を追跡することによる、ソフトウェアプログラムの分析を示す。この分析は、記号の変数としてソフトウェアモジュールへの入力を扱う明示的でない状態モデルのチェック技術である。この技術は、記号変数をもつソフトウェアモジュールにおいて全ての有限の経路を実行することで複雑な数学的な式又は表現を作り出し、次いで、複雑な式を決定手順として典型的に知られる解法により解いて、もしあればエラーのシナリオを得る。明示的な状態モデルのチェックとは対照的に、記号的実行は、全ての可能性のある入力値と、分析下にあるソフトウェアモジュールにおける全ての入力変数の全ての可能性のある使用のケースを解明することができる。記号的実行を更に説明するため、fooと名付けられた例示的なソフトウェアモジュールを考える。ソフトウェアモジュールfooは、2つの入力変数a及びbを有し、2つのローカル変数c及びdを有する。特定の実施の形態では、ローカル変数の値は、直接的又は間接的に、ソフトウェアモジュールの1以上の入力変数の値に依存する。たとえば、モジュールfooにより、ローカル変数cの値は、コードのライン3により示されるように、入力変数a及びbの値に直接的に依存し、ローカル変数dの値は、コードのライン5により示されるように、ローカル変数cを通して、入力変数a及びbの値に間接的に依存する。さらに、モジュールfooは、ifelse命令文により生じる、コードのライン4での条件分岐点を含む。ライン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が割り当てられる。変数a、b、c及びdは、stringのタイプからなるので、記号値x、y、z及びwは、任意の文字列をそれぞれ表す。さらに、Φは、実行経路に沿った様々なポイントでの記号的実行の結果を表す記号的表現である。より詳細には、モジュールfooのコードのライン2に対応する802で、変数a、b、c及びdには、それぞれの記号の値x、y、z及びwが割り当てられ、Φは、空又はゼロの表現を最初に有する。実行が更に進行するとき、コードが実行されているかに依存して式がΦに追加される。モジュールfooのコードのライン3に対応する804で、Φは、式zconcatを有する。これは、コードのライン3がcaconcatであり、x、y及びzが変数a、b及びcにそれぞれ割り当てられた記号値であるからである。つぎに、モジュールfooのコードのライン4は、条件分岐点であり、実行が進行する2つの可能性のある実行経路が存在する。従って、記号的実行は、2つの異なる経路に進行し、第一の経路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の式は、zconcattとして書き換えられる。808は、PATH1の終わりであり、従って808でのΦの式は、PATH1の実行の終わりに到達するために満たされる必要がある、記号の形式での条件を表す。同様に、810は、PATH2の実行の終わりであり、従って801でのΦの式は、PATH2の終わりに到達するために満たされる必要がある、記号の形式での条件を表す。モジュールfooは2つの可能性のある実行経路を有するので、モジュールfooを記号的に実行することで、2つの式のセットが得られ、2つの式のセットのそれぞれは、それぞれの実行経路に対応する。特定の実施の形態では、808でΦの式を解くことで、モジュールfooにPATH1の終わりに到達させる入力変数a及びbの実際の値が与えられ、810でΦの式を解くことで、モジュールfooにPATH2の終わりに到達させる入力変数a及びbの実際の値が与えられる。ソフトウェアモジュールで記号的実行を行うことから得られる式のセットを解くため、特定の実施の形態は、図7のステップ704に示されるように、ソフトウェアモジュールの変数に課される制約のセットとして、しれぞれの式のセットを表現する。たとえば、モジュールfooにより、808での式のセットは、a、b、c及びdに課される制約のセットtとして表現される。810での式のセットは、a、b、c及びdに課される制約のセットとして表現される。ソフトウェアモジュールでの記号的実行を行うことから得られるそれぞれの制約のセットについて、特定の実施の形態は、適用可能な数式としてセットからのそれぞれの数値の制約と、アプリケーションFSMとしてセットからのそれぞれの文字列の制約とを表現する。図9Aは、ソフトウェアモジュールの3つの対応する実行経路912,914,916と共に、例示的なソフトウェアモジュールについて決定された3つの例示的な制約のセット902,904及び906を示し、この場合、数値の制約は、数式として表現され、文字列の制約は、FSMとして表現される。この例示的なソフトウェアモジュールを検査するため、それぞれの経路912,914及び916の終わりで、それぞれの対応する制約のセット902,904及び906は、テストケースについて解かれる。特定の実施の形態は、図1に示されるプロセスを使用して、図7のステップ706に示されるように、それぞれの制約のセットについて1以上の解を発見するのを試み、次いで、図7のステップ708に示されるように、テストの入力として発見された解を使用して、ソフトウェアモジュールを検査する。特定の実施の形態では、制約のセットの解は、セットにおける全ての制約を満たす制約が課される変数について実際の値を含む。ソフトウェアモジュールを検査するとき、これらの実際の解の値は、テストの入力としてソフトウェアモジュールの変数に割り当てられる。制約のセットについて発見された解が与えられると、解の値は対応する制約のセットからの全ての制約を共に満たし、且つ、ソフトウェアモジュールへのテスト入力として実際の値すなわち、制約のセットについて発見された解からの値の特定の組み合わせを適用することで、特定の実行経路に沿って進行して、特定の実行経路の終わりに到達するときに、制約のセットはソフトウェアモジュールの状態を表すたとえば、記号的実行から取得された式のセットに対応するので、ソフトウェアモジュールが特定の実行経路に沿って進行して、特定の実行経路の終わりに到達することが保証される。結果として、これら特定の解の値がテスト入力としてソフトウェアモジュールの対応する変数に割り当てられた場合に、特定の実行経路は、完全に検査される。さらに、ある解がソフトウェアモジュールのありとあらゆる実行経路について得られたありとあらゆる式のセットに対応するありとあらゆる制約のセットについて発見され、且つ解の値がたとえば、同時に1つの解の実際の値を適用することでテスト入力としてソフトウェアモジュールに適用された場合、ソフトウェアモジュールの全ての可能性のある実行経路は、十分にテストされる。ソフトウェアモジュールの実行経路の何れかにおいてエラーが存在する場合、係るシステマチックな検査は、エラーを最終的に見つけることができる。特定の実施の形態では、図1に示されるようなプロセスは、ソフトウェアモジュールの設計又は仕様の要件が満たされるかを検証するために使用される。典型的に、所与のソフトウェアモジュールに関連する正式な設計又は仕様の要件が存在する。これらの形式的な要件の幾つかは、ソフトウェアモジュールの入力又は出力に課される。特定の実施の形態では、ソフトウェアモジュールの入力に課される仕様の要件は、ソフトウェアモジュールに関連する前提条件と呼ばれ、ソフトウェアモジュールの出力に課される仕様の要件は、ソフトウェアモジュールに関連する事後条件と呼ばれる。この事後条件は、ソフトウェアモジュールに関連する前提条件に依存する。先に説明されたように、ソフトウェアモジュールは、たとえばifelse命令文といった任意の数の条件分岐点を含み、それぞれの条件分岐点は、ソフトウェアモジュールのたとえば入力変数又はローカル変数といった1以上の変数により指定される分岐条件を有する。分岐条件が満たされたかに依存して、ソフトウェアモジュールは、異なる実行経路に進む。従って、ソフトウェアモジュールが実行されたとき、ソフトウェアモジュールに含まれる条件分岐点から得られる可能性のある実行経路のうちの何れか1つに進む。結果的に、特定の実施の形態では、ソフトウェアモジュールがその入力と出力に課された形式的な仕様の要件すなわち、ソフトウェアモジュールに関連する前提条件及び事後条件を満たすかを検証するとき、ソフトウェアモジュールの全ての可能性のある実行経路について、ソフトウェアモジュールに関連する前提条件及び事後条件が当てはまる場合且つその場合に限り、ソフトウェアモジュールは、検証テストを通過したすなわち、仕様の要件を満たしたと見なされる。図10は、たとえば形式的な設計又は仕様の要件といったソフトウェアモジュールの入力と出力に課される要件すなわち、ソフトウェアモジュールに関連する前提条件及び事後条件に関連して、ソフトウェアモジュールを検証する例示的な方法を示す。特定の実施の形態は、図10のステップ102で示されるように、ソフトウェアモジュールのたとえば、入力変数に課される要件といったそれぞれの前提条件、及びたとえば出力変数に課される要件といったそれぞれの事後条件を、ソフトウェアモジュールの入力又は出力変数に課される制約として表現する。たとえば、文字列のタイプからなる2つの入力変数a及びbを有する例示的なソフトウェアモジュールfooを考える。先に例示されたように、fooのコードに基づいて、fooは、文字列のタイプからなる1つの出力値をリターンすることが判定される。すなわち、fooは、文字列のタイプからなる1つの出力変数を有する。pをfooの出力変数を表すものとする。ソフトウェアfooの使用により指定され、且つa、b及びpに課される制約として表現されたとき、a、b及びpに課される前提条件及び事後条件は、以下の通りであるとする。次いで、特定の実施の形態は、図10のステップ1004に示されるように、ソフトウェアモジュールの事後条件を否定する。先の例におけるように、ソフトウェアモジュールは、1つの事後条件pendsWithを有する。この事後条件を論理的に否定することで、が得られる。特定の実施の形態は、図10のステップ1006に示されるように、ソフトウェアモジュールのそれぞれの可能性のある実行経路に対応する制約のセットを取得し、次いで、それぞれの制約のセットに前提条件及び否定された事後条件を組み入れるため、ソフトウェアモジュールでの記号的実行を行う。記号的実行は、図7のステップ702と共に上述されており、ここでは同様に実行される。それぞれの制約のセットを決定するとき、特定の実施の形態は、もしあればたとえば図1のステップ104と共に記載されるソフトウェアモジュールの特定の変数について推定された数値及び文字列の制約と同様に、もしあれば図1のステップ102と共に記載されるソフトウェアモジュールの特定の変数に最初に課された数値及び文字列の制約を組み入れる。たとえば、ソフトウェアモジュールfooは、図8に示されたような、2つの可能性のある実行経路を有する。従って、ソフトウェアモジュールfooで記号的実行を行うことで、2つの式のセットが得られる。第一の経路PATH1について、fooに記号的実行を行うことから得られた式のセットは、図8の808により示されるように、tqrsとして書き換えられる。なお、dはPATH1の終わりでfooによりリターンされる値すなわちfooの出力であり、wはdに割り当てられた記号値であるので、pはPATH1についてdの値を有する。さらに、xはaに割り当てられた記号値であり、bはyに等価であり、且つzはcに等価であるので、aはxに等価であり、これは、fooのソースコードに従ってconcatに等しい。次いで、前提条件及び否定された事後条件は、この制約のセットに追加される。従ってPATH1の最終的な制約のセットは、tqrsとなる。第二の経路PATH2について、fooで記号的実行を行うことから得られた式のセットは、図8の810により示されるように、qrsとして書き換えられる。なお、cはPATH2の終わりでfooによりリターンされた値すなわち、fooの出力であり、zはcに割り当てられた記号値であるため、pはPATH2についてcの値を有し、これは、fooのソースコードに従ってconcatに等しい。次いで、前提条件及び否定された事後条件は、この制約のセットに同様に追加される。PATH2について最終的な制約のセットは、qrsとなる。次いで、特定の実施の形態は、図1に示されたプロセスを使用して、図10のステップ1008に示されるように、ソフトウェアモジュールのそれぞれの可能性のある実行経路に対応するそれぞれの制約のセットについて1以上の解を発見するのを試みる。それぞれの制約のセットは、ソフトウェアモジュールに関連する前提条件と否定された事後条件と同様に、ソフトウェアモジュールで記号的実行を行うことから得られた制約を含む。特定の実施の形態では、ソフトウェアモジュールの特定の実行経路に対応するそれぞれの制約のセットについて、そのセットからの全ての制約を満たす解が発見されない場合、この実行経路について、ソフトウェアモジュールは、前提条件及び事後条件により表されるように、その入力と出力に課される要件を満たす。図10のステップ1004及び1006で説明されたように、ソフトウェアモジュールの出力で課された否定された事後条件をそれぞれの制約のセットが含むことを思い出されたい。従って、この制約のセットについて解が発見されない場合すなわち、制約のセットが満足されない場合、より詳細には、否定された事後条件を満たす解が発見されない場合、前提条件及び事後条件は、対応する実行経路について当てはまることを意味する。逆に、そのセットからの全ての制約を満たす解が発見された場合、対応する実行経路について、前提条件及び事後条件がその実行経路について当てはまらないため、ソフトウェアモジュールは、その入力と出力で課される要件を満たさない。逆に、図10のステップ1006で得られた制約のセットについて解が発見された場合、ソフトウェアモジュールは、入力と出力に課される要件に関連して検証テストを通過しない。図10のステップ1006で得られたありとあらゆる制約のセットが満たされないときにのみ、ソフトウェアモジュールは、その入力と出力で課された要件に関して検証テストを通過する。図9Bは、ソフトウェアモジュールの3つの対応する実行経路912,914及び916と共に、図9Aに示されるように、例示的なソフトウェアモジュールについて決定される3つの例示的な制約のセット902,904及び906を示す。ソフトウェアモジュールの入力と出力に課される要件に関連して、この例示的なソフトウェアモジュールを検証するため、それぞれの経路912,914及び916の終わりで、それぞれの対応する制約のセット902,904及び906は、要件及びアサーションについて解かれる。特定の実施の形態では、図1に示されたようなプロセスは、インジェクション攻撃を検出して捕捉するために設計されるソフトウェアモジュールを検証するために使用される。インサーション攻撃としても知られるインジェクション攻撃は、SQLデータベース及び他の脆弱なウェブサイトをしばしば標的にする悪意のあるソフトウェア攻撃の形態である。一般に、SQLインジェクションは、ソフトウェアアプリケーションのデータベースレイヤで生じるセキュリティの脆弱性を利用する符号注入技術である。脆弱性は、あるプログラミング言語又はスクリプト言語が別のプログラミング言語又はスクリプト言語内に埋め込まれるときは何時でも生じる。より詳細には、SQLステートメントに埋め込まれた文字列の文字列リテラルのエスケープ文字についてユーザ入力が誤ってフィルタリングされたとき、又はユーザ入力が強くタイプされず、これにより突然に実行されたときに、脆弱性が存在する。たとえば、インジェクション攻撃は、qkd1shutdownsqdとしてたとえばランダムな文字のセットといった別の文字列に文字列shutdownを埋め込み、この文字列を入力コマンドたとえばSQL命令文としてデータベースに送出する。データベースソフトウェアが、一見したところランダムな入力文字列に埋め込まれたshutdown文字列を捕捉して、それを実行しない場合、shutdown文字列は、データベースに不注意にシャットダウンさせる場合がある。結果として、大部分のデータベースは、係るインジェクション攻撃を検出して捕捉するために設計されたソフトウェアモジュールを有する。特定の実施の形態では、図1に示されたプロセスは、係るセキュリティソフトウェアモジュールがインジェクション攻撃として入力に埋め込まれた多くの異なる形式の悪意のある文字列を検出することができるかを検証するために使用される。たとえば、セキュリティソフトウェアモジュールを検査する1つの方法は、悪意のある文字列を考えるか、たとえば、悪意のある文字列が無害であると信じるようにセキュリティソフトウェアモジュールをだますといったセキュリティソフトウェアモジュールがそれを検出できないように、悪意のある文字列を埋め込むことである。図11は、インジェクション攻撃を検出するために設計されたセキュリティソフトウェアモジュールを検証する例示的な方法を示す。特定の実施の形態では、セキュリティソフトウェアモジュールは、任意の悪意のある文字列を入力文字列が含むかを検証するため、セキュリティソフトウェアモジュールに通過されるたとえば、入力文字列といった入力値に様々なセキュリティチェックを実行する。それぞれのセキュリティチェックポイントで、入力値がセキュリティチェックを通過した場合、セキュリティソフトウェアモジュールは、次のセキュリティチェックポイントに進む。さもなければ、セキュリティソフトウェアモジュールは、たとえばFALSEをリターンするといった入力値が特定のセキュリティチェック失敗したことの指示をリターンする。入力文字列がセキュリティソフトウェアモジュールに含まれる全てのセキュリティチェックを通過したときにのみ、セキュリティソフトウェアモジュールは、入力値が無害であることの指示をリターンするたとえばTRUEをリターンする。特定の実施の形態は、図11のステップ1102に示されるように、インジェクション攻撃に関連して使用される可能性があるshutdownのような悪意のある文字列のセットを選択する。mを特定の悪意のある文字列を表すとする。特定の実施の形態は、図11のステップ1104に示されるように、sにより表される別の文字列に、セットからのそれぞれの悪意のある文字列を埋め込む。sにおいて、悪意のある文字列の前に幾つかの文字すなわちサブ文字列があり、悪意のある文字列の後の幾つかの文字すなわち、別のサブ文字列がある場合がある。従って、sは、sconcatyとして表現され、この場合、xは、sにおける、悪意のある文字列mの前にあるサブ文字列を表し、yは、悪意のある文字列mの後にあるサブ文字列を表す。なお、x又はyの何れかは、空の文字列であり、mは、sの別のサブ文字列となる。文字列sは、入力値としてセキュリティソフトウェアモジュールに適用される。特定の実施の形態は、図11のステップ1106に示されるように、制約が満足される場合、セキュリティソフトウェアモジュールにその終わりにまで実行させ、入力値がモジュールに含まれる全てのセキュリティチェックを上手く通過したことの指示をリターンさせる制約のセットを取得するため、セキュリティソフトウェアモジュールで記号的実行を行う。記号的実行は、図7のステップ702と関連して上述され、本実施の形態で同様に実行される。制約のセットを決定するとき、特定の実施の形態は、もしあれば、図1のステップ104に関連して記載されるようにソフトウェアモジュールの特定の変数について推定された数値及び文字列の制約と同様に、もしあれば、たとえば図1のステップ102に関連して記載されるようにソフトウェアモジュールの特定の変数に最初に課される数値及び文字列の制約を組み入れる。特定の実施の形態では、このように得られた制約のセットは、入力値が無害であることを示す出力値をソフトウェアモジュールがリターンするように、セキュリティソフトウェアモジュールに含まれる全てのセキュリティチェックを上手く通過するため、セキュリティソフトウェアモジュールの入力変数に割り当てられた入力値について満たされる必要がある全ての制約を表す。特定の実施の形態は、図1に示されるプロセスを使用して、図11のステップ1108に示されるように、sが全ての制約を満たすように、それぞれの悪意のある文字列が埋め込まれているとき、sについて1以上の解を発見しようと試みる。任意の解が制約のセットを満たすsについて発見された場合、セキュリティソフトウェアモジュールに含まれる全てのセキュリティチェックを通過するのを間違えたsに埋め込まれた少なくとも1つの悪意のある文字列が存在することを意味する。結果的に、セキュリティソフトウェアモジュールは、インジェクション攻撃に対して脆弱性がある。例として悪意のある文字列shutdownを使用する。この文字列をsに埋め込むことで、sconcatyが得られる。図1に示されるプロセスを使用して、特定の実施の形態は、埋め込まれたshutdownをもつsがセキュリティソフトウェアモジュールで記号的実行を行うことから得られる制約のセットからの全ての制約を満たすように、サブ文字列x及びyの値を与えるsの解が存在するかを発見するのを試みる。x及びyの解が存在する場合、セキュリティソフトウェアモジュールに含まれる全てのセキュリティチェックを文字列sが上手く通過するようにすなわち、セキュリティソフトウェアモジュールが悪意のある文字列shutdownが埋め込まれたこの特定のインジェクション攻撃を検出することができないように、値concatyを有する文字列sに悪意のある文字列shutdownを埋め込む少なくとも1つの方法が存在することを意味する。特定の実施の形態では、それぞれの悪意のある文字列は、文字列sに埋め込まれたとき、異なるデータタイプを使用して表現される。たとえば、16進数として表現される文字列shutdownは、0x73687574646f776eとして表現される。従って、sについて1つの可能性のある値は、文字列のデータタイプにおける悪意のある文字列を表現するexecshutdownであり、sについて別の可能性のある値は、整数のデータ対応で悪意のある文字列を表現するdeclareacharselecta0x73687574646f776eexecである。特定の実施の形態は、sについて解を発見することを試み、この場合、埋め込まれた悪意のある文字列は、異なるデータタイプを使用して表現される。結果として、セキュリティソフトウェアモジュールは、従来の文字列データで表される悪意のある文字列で検査されるだけでなく、たとえば整数又は浮動小数点数として表される予期しないデータタイプで表される悪意のある文字列でも検査される。特定の実施の形態は、sが文字列全体としてすなわちx、m及びyを含めて図11のステップ1106から得られる制約のセットを満たすようにsにおいて悪意のある文字列のセットからそれぞれの悪意のある文字列mを埋め込み、次いでx及びyの特定の値を提供するsの解を発見するのを試みる。sに埋め込まれた悪意のある文字列mをもつsについて解が発見された場合、セキュリティソフトウェアモジュールは、対応するインジェクション攻撃を検出することができず、従って脆弱であることを意味する。さらに、sに埋め込まれた悪意のある文字列mをもつsについて解が発見されない場合、特定の実施の形態は、図11のステップ1106から得られた制約のセットを満たす解を発見しようと試みる。解が発見された場合、特定の実施の形態は、解それ自身が実際に悪意のある文字列であるかを検証する。このセキュリティソフトウェアモジュールに関する検証は、悪意のある文字列が、それ自身において別の文字列に埋め込まれることなしに、セキュリティソフトウェアモジュールに含まれる全てのセキュリティチェックを上手く通過することができるかすなわち、セキュリティソフトウェアモジュールが悪意のある文字列を検出することができないことを判定することを試みる。図9Cは、ソフトウェアモジュールの3つの対応する実行経路912,914及び916と共に、図9Aに示されるように、例示的なソフトウェアモジュールについて決定された3つの例示的な制約のセット902,904及び906を示す。例示的なソフトウェアモジュールが例示的なセキュリティソフトウェアモジュールである場合、この例示的なセキュリティソフトウェアモジュールを検証するため、それぞれの経路912,914及び916の終わりで、それぞれ対応する制約のセット902,904及び906は、ソフトウェアの内部チェックを通過した全ての可能性のある文字列を表すホットスポットFSMと、悪意のあるFSMとの交点について解かれる。交点がゼロである場合、可能性のあるインジェクション攻撃が発見されない。ゼロでない交点は、可能性のあるインジェクション攻撃の文字列を即座に示す。特定の実施の形態は、ネットワーク環境で実現される。図12は、サービスとしてソフトウェア検証を提供するのに適した例示的なネットワーク環境を示す。ネットワーク環境1200は、1以上のサーバ1220と1以上のクライアント1230を互いに結合するネットワーク1210を含む。特定の実施の形態では、ネットワーク1210は、イントラネット、エクストラネット、VPNVirtualPrivateNetwork、LANLocalAreaNetwork、無線LAN、WANWideAreaNetwork、MANMetropolitanAreaNetwork、インターネットの一部、又は別のネットワーク1210、又は2以上の係るネットワーク1210の組み合わせである。本発明は、適切なネットワーク1210を含んでいる。1以上のリンク1250は、サーバ1220又はクライアント1230をネットワーク1210に結合する。特定の実施の形態では、1以上のリンク1250は、1以上の有線、無線又は光リンク1250をそれぞれ含む。特定の実施の形態では、1以上のリンク1250は、イントラネット、エクストラネット、VPN、LAN、WLAN、WAN、MAN、インターネットの一部、又は別のリンク1250、或いは2以上の係るリンク1250の組み合わせを含む。本発明は、サーバ1220及びクライアント1230をネットワーク1210に結合する適切なリンク1250を含む。特定の実施の形態では、それぞれのサーバ1220は、単一のサーバであるか、或いは、複数のコンピュータ又は複数のデータセンタに及ぶ分散サーバである。サーバ1220は、たとえば限定されるものではないが、ウェブサーバ、ニュースサーバ、メールサーバ、メッセージサーバ、広告サーバ、ファイルサーバ、アプリケーションサーバ、エクスチェンジサーバ、データベースサーバ又はプロキシサーバのような様々なタイプからなる場合がある。特定の実施の形態では、それぞれのサーバ1220は、ハードウェア、ソフトウェア、又は埋め込みロジックコンポーネント、或いは、サーバ1220により実現又はサポートされる適切な機能を実行する2以上の係るコンポーネントの組み合わせを含む場合がある。たとえば、ウェブサーバは、ウェブページ又はウェブページの特定のエレメントを含むウェブサイトを主催することができる。より詳細には、ウェブサーバは、HTMLファイル又は他のファイルタイプを主催するか、要求に応じてファイルを動的に作成又は構成し、それらをHTTP又はクライアント1230からの他の要求に応答してクライアント1230に伝達する。メールサーバは、電子メールサービスを様々なクライアント1230に提供可能である。データベースサーバは、1以上のデータストアに記憶されるデータを管理するインタフェースを供給可能である。特定の実施の形態では、1以上のデータストレージ1240は、1以上のリンク1250を介して1以上のサーバ1220にリンクされる。特定の実施の形態では、データストレージ1240は、様々な情報のタイプを記憶するために使用される。特定の実施の形態では、データストレージ1240に記憶される情報は、特定のデータ構造に従って編成される。特定の実施の形態では、それぞれのデータストレージ1240は、リレーショナルデータベースである。特定の実施の形態は、サーバ1220又はクライアント1230が、たとえばデータストレージ1240に記憶される情報を検索、修正、追加又は削除といった、情報を管理するのを可能にするインタフェースを提供する。特定の実施の形態では、それぞれのクライアント1230は、ハードウェア、ソフトウェア、又は埋め込みロジックコンポーネント、或いはクライアント1230により実現又はサポートされる適切な機能を実行可能な2以上の係るコンポーネントの組み合わせを含む電子装置である。たとえば限定されることなしに、クライアント1230は、デスクトップコンピュータシステム、ノートブックコンピュータシステム、ネットブックコンピュータシステム、ハンドヘルド電子装置、又は移動電話である場合がある。本発明は、適切なクライアント1230を含む。クライアント1230は、クライアント1230でのネットワークユーザがネットワーク1230にアクセスするのを可能にする。クライアント1230は、そのユーザが他のクライアント1230で他のユーザと通信するのを可能にする。クライアント1230は、MICROSOFTINTERNETEXPLORER、GOOGLECHROME又はMOZILLAFIREFOXのようなウェブブラウザ1232を有し、1以上のアッドオン、プラグイン又はTOOLBAR又はYAHOOTOOLBARのような他の拡張を有する。クライアント1230でのユーザは、URLUniformResourceLocator、又はウェブブラウザ1232をサーバ1220に向ける他のアドレスを入力し、ウェブブラウザ1232は、HTTPHyperTextTransferProtocol要求を生成し、HTTP要求をサーバ1220に伝達する。サーバ1220は、HTTP要求を受けて、HTTP要求に応じて、1以上のHTMLHyperTextMarkupLanguageファイルをクライアント1230に伝達する。クライアント1230は、ユーザへの提示のため、サーバ1220からのHTMLファイルに基づいてウェブページをレンダリングする。本発明は、適切なウェブページのファイルを含む。例として、限定されるものではないが、ウェブページは、特定の必要に応じて、HTMLファイル、XHTMLExtensibleHyperTextMarkupLanguageファイル、又はXMLExtensibleMarkupLanguageファイルからレンダリングされる。また、係るページは、たとえば限定されるものではないが、JAVASCRIPT、JAVA、MICROSOFTSILVERLIGHT、AJAXAsynchronousJAVASCRIPT及びXMLのようなマークアップ言語とスクリプト言語の組み合わせ等で書かれたもののようなスクリプトを実行する。ここで、あるウェブページの参照は、ブラウザがウェブページをレンダリングするために使用する1以上の対応するウェブページファイルを包含し、逆に、1以上の対応するウェブページファイルは、ウェブページを包含する。特定の実施の形態は、1以上のコンピュータシステムで実現される。図13は、例示的なコンピュータシステム1300を示す。特定の実施の形態では、1以上のコンピュータシステム1300は、本実施の形態で記載される1以上の方法の1以上のステップを実行する。特定の実施の形態では、1以上のコンピュータシステム1300は、本実施の形態で記載又は図示される機能を提供する。特定の実施の形態では、1以上のコンピュータシステム1300で実行されているソフトウェアは、本実施の形態で記載又は図示される1以上の方法の1以上のステップを実行するか、又は本実施の形態で記載又は図示される機能を提供する。特定の実施の形態は、1以上のコンピュータシステム1300の1以上の部分を含む。本発明の開示は、適切な数のコンピュータシステム1300を含む。本発明の開示は、適切な物理的な形態を取るコンピュータシステム1300を含む。例として限定されるものではないが、コンピュータシステム1300は、埋め込みコンピュータシステム、システムオンチップSOC、たとえばコンピュータオンモジュールCOM、システムオンモジュールSOMのようなシングルボードコンピュータシステムSBC、デスクトップコンピュータシステム、ラップトップ又はノートブックコンピュータシステム、インタラクティブキオスク、メインフレーム、コンピュータシステムのメッシュ、モバイルフォン、パーソナルデジタルアシスタントPDA、サーバ、又はこれらの2以上の組み合わせである場合がある。必要に応じて、コンピュータシステム1300は、単一であるか又は分散であるか、複数の位置に及ぶか、複数のコンピュータに及ぶか、或いは、1以上のネットワークにおいて1以上のクラウドコンポーネントを含むクラウドにある1以上のコンピュータシステム1300を含む。必要に応じて、1以上のコンピュータシステム1300は、実質的な空間又は時間的な制限なしに、本実施の形態で記載又は図示された1以上の方法の1以上のステップを実行する。例として限定されるものではないが、1以上のコンピュータシステム1300は、本実施の形態で記載又は図示された1以上の方法の1以上のステップをリアルタイムで実行するか、バッチモードで実行する。1以上のコンピュータシステム1300は、必要に応じて、本実施の形態で記載又は図示される1以上の方法の1以上のステップを異なる時間又は異なる位置で行う。特定の実施の形態では、コンピュータシステム1300は、プロセッサ1302、メモリ1304、ストレージ1306、入力/出力IOインタフェース1308、通信インタフェース1310及びバス1312を含む。本発明の開示は、特定の配置において特定の数の特定の構成要素を有する特定のコンピュータシステムを記載及び図示しているが、本発明の開示は、適切な配置における適切な数の構成要素を有する適切なコンピュータシステムを含む。特定の実施の形態では、プロセッサ1302は、コンピュータプログラムを作成する命令のような命令を実行するハードウェアを含む。例として限定されるものではないが、命令を実行するため、プロセッサ1302は、内部レジスタ、内部キャッシュ、メモリ1304又はストレージ1306からの命令を検索又はフェッチし、それらをデコード及び実行し、次いで、1以上の結果を内部レジスタ、内部キャッシュ、メモリ1304又はストレージ1306に書き込む。特定の実施の形態では、プロセッサ1302は、データ、命令又はアドレスのための1以上の内部キャッシュを含む。本発明の開示は、必要に応じて、適切な数の適切な内部キャッシュを含むプロセッサ1302を含む。例として限定されるものではないが、プロセッサ1302は、1以上の命令キャッシュ、1以上のデータキャッシュ、及び1以上のTLBTranslationLookasideBuffersを含む。命令キャッシュにおける命令は、メモリ1304又はストレージ1306における命令のコピーである、命令キャッシュは、プロセッサ1302により命令の検索を高速にする。データキャッシュにおけるデータは、プロセッサ1302で動作を実行させる命令のためのメモリ1304又はストレージ1306におけるデータのコピー、プロセッサ1302で実行するその後の命令によりアクセスするか又はメモリ1304又はストレージ1306への書き込みのためにプロセッサ1302で実行された前の命令の結果、その他の適切なデータである。データキャッシュは、プロセッサ1302による読み取り又は書き込み動作を高速にする。TLBは、プロセッサ1302について仮想的なアドレス変換を高速にする。特定の実施の形態では、プロセッサ1302は、データ、命令又はアドレスのために1以上の内部レジスタを含む。本発明の開示は、必要に応じて、任意の数の適切な内部レジスタを含むプロセッサ1302を含む。必要に応じて、プロセッサ1302は、マルチコアプロセッサである1以上のALUArithmeticLogicUnitを含むか、又は1以上のプロセッサ1302を含む。本発明の開示は特定のプロセッサを記載及び図示しているが、本発明の開示は、適切なプロセッサを含んでいる。特定の実施の形態では、メモリ1304は、プロセッサ1302が実行するための命令又はプロセッサ1302が動作するデータを記憶するメインメモリを含む。例示として限定されるものではないが、コンピュータシステム1300は、ストレージ1306又はたとえば別のコンピュータシステム1300のような別のソースからメモリ1304に命令をロードする。プロセッサ1302は、メモリ1304から内部レジスタ又は内部キャッシュに命令をロードする。命令を実行するため、プロセッサ1302は、内部レジスタ又は内部キャッシュからの命令を検索し、それらをデコードする。命令の実行の間又は実行の後、プロセッサ1302は、中間又は最終的な結果である1以上の結果を内部レジスタ又は内部キャッシュに書き込む。プロセッサ1302は、1以上の結果をメモリ1304に書き込む。特定の実施の形態では、プロセッサ1302は、ストレージ1306又はその他とは対照的に1以上の内部レジスタ又は内部キャッシュ或いはメモリ1304における命令のみを実行し、ストレージ1306又はその他とは対照的に1以上の内部レジスタ又は内部キャッシュ或いはメモリ1304におけるデータに関してのみ動作する。アドレスバス及びデータバスをそれぞれ含む1以上のメモリバスは、プロセッサ1302をメモリ1304に結合する。バス1312は、以下に記載されるように1以上のメモリバスを含む。特定の実施の形態では、1以上のメモリ管理ユニットMMUは、プロセッサ1302とメモリ1304との間にあり、プロセッサ1302により要求されたメモリ1304へのアクセスを容易にする。特定の実施の形態では、メモリ1304は、ランダムアクセスメモリRAMを含む。このRAMは、必要に応じて、揮発性メモリである。必要に応じて、このRAMは、DRAMDynamicRAM又はSRAMStaticRAMである。さらに、必要に応じて、このRAMは、シングルポート又はマルチポートRAMである。本発明の開示は、適切なRAMを含んでいる。メモリ1304は、必要に応じて、1以上のメモリ1304を含む。本発明の開示は特定のメモリを記載及び図示しているが、本発明の開示は、適切なメモリを含んでいる。特定の実施の形態では、ストレージ1306は、データ又は命令のための大容量ストレージを含む。例として限定されるものではないが、ストレージ1306は、HDD、フロッピーディスクドライブ、フラッシュメモリ、光ディスク、光磁気ディスク、磁気テープ又はUSBUniversalSerialBusドライブ又はこれらの2以上の組み合わせを含む。ストレージ1306は、必要に応じて、取り外し可能又は取り外し不可能すなわち固定された媒体を含む。ストレージ1306は、必要に応じて、コンピュータシステム1300の内部又は外部にある。特定の実施の形態では、ストレージ1306は、不揮発性の固体メモリである。特定の実施の形態では、ストレージ1306は、リードオンリメモリROMを含む。必要に応じて、このROMは、マスクプログラムROM、プログラマブルROM、PROM、消去可能なROMEPROM、電子的に消去可能なPROMEEPROM、電子的に変更可能なROMEAROM、又はフラッシュメモリ或いはこれらの2以上の組み合わせである。本発明の開示は、適切な物理的な形式を取る大容量ストレージ1306を含む。ストレージ1306は、必要に応じて、プロセッサ1302とストレージ1306間の通信を容易にする1以上の記憶制御装置を含む。必要に応じて、ストレージ1306は、1以上のストレージ1306を含む。本発明の開示は、特定のストレージを記載及び図示しているが、本発明の開示は、適切なストレージを含む。特定の実施の形態では、IOインタフェース1308は、コンピュータシステム1300と1以上のIO装置との間の通信のための1以上のインタフェースを提供するハードウェア、ソフトウェア、又はその両者を含む。コンピュータシステム1300は、必要に応じて、1以上のこれらIO装置を含む。1以上のこれらIO装置は、ある人物とコンピュータシステム1300との間の通信を可能にする。例示として限定されるものではないが、IO装置は、キーボード、キーパッド、マイクロフォン、モニタ、マウス、プリンタ、スキャナ、スピーカ、スチルカメラ、スタイラス、タブレット、タッチスクリーン、トラックボール、ビデオカメラ、別の適切なIO装置、或いはこれらの2以上の組み合わせを含む場合がある。IO装置は、1以上のセンサを含む。本発明の開示は、適切なIO装置及びこれらIO装置のために適切なIOインタフェースを含んでいる。必要に応じて、IOインタフェース1308は、プロセッサ1302が1以上のこれらのIO装置を駆動するのを可能にする1以上のデバイス又はソフトウェアドライバを含む。IOインタフェース1308は、必要に応じて、1以上のIOインタフェース1308を含む。本発明の開示は特定のIOインタフェース1308を記載及び図示しているが、本発明の開示は、適切なIOインタフェースを含んでいる。特定の実施の形態では、通信インタフェース1310は、コンピュータシステム1300と1以上の他のコンピュータシステム1300又は1以上のネットワークとの間でたとえばパケットに基づく通信のような通信のための1以上のインタフェースを提供するハードウェア、ソフトウェア又はこれらの両者を含む。例示として限定されるものではないが、通信インタフェース1310は、Eithernet又は他の有線に基づくネットワークと通信するネットワークインタフェースコントローラNIC又はネットワークアダプタ、又は、WIFIネットワークのような無線ネットワークと通信する無線NICWNIC又は無線アダプタを含む。本発明の開示は、適切なネットワーク及び該ネットワークのための適切な通信インタフェース1310を含んでいる。例示として限定されるものではないが、コンピュータシステム1300は、アドホックネットワーク、PANPersonalAreaNetwork、LANLocalAreaNetwork、WANWideAreaNetwork、MANMetropolitanAreaNetwork又は1以上のインターネットの部分、或いはこれらの2以上の組み合わせと通信する。1以上のこれらのネットワークの1以上の部分は、有線又は無線である。例として、コンピュータシステム1300は、たとえばBLUETOOTHWPANのような無線PANWPAN、WIFIネットワーク、WIMAXネットワーク、たとえばGSMGlobalSystemforMobileCommunicationネットワークのような携帯電話網、又は他の適切な無線ネットワーク、或いはこれらの2以上の組み合わせと通信する場合がある。コンピュータシステム1300は、必要に応じて、これらのネットワークの何れかのために適切な通信インタフェース1310を含む。通信インタフェース1310は、必要に応じて、1以上の通死人タフェース1310を含む。本発明の開示は特定の通死人タフェースを記載及び図示しているが、本発明の開示は、適切な通信インタフェースを含んでいる。特定の実施の形態では、バス1312は、コンピュータシステム1300の構成要素を互いに結合するハードウェア、ソフトウェア又はこれらの両者を含む。例示として限定されるものではないが、バス1312は、AGPAcceleratedGraphicsPort又は他のグラフィックスバス、EISAEnhancedIndustryStandardArchitectureバス、フロントサイドバスFSB、HYPERTRANSPORTHTインターコネクト、LPCLowPinCountバス、メモリバス、MCAMicroChannelArchitectureバス、PCIPeripheralComponentInterconnectバス、PCIEXPCIExpressバス、SATASerialAdvancedTechnologyAttachmentバス、VLBVideoElectronicsStandardsAssociationlocalバス、又は別の適切なバス、或いはこれらの2以上の組み合わせを含む場合がある。バス1312は、必要に応じて、1以上のバス1312を含む。本発明の開示は特定のバスを記載及び図示するものであるが、本発明の開示は、適切なバス又はインターコネクトを含んでいる。ここで、コンピュータ読み取り可能な記録媒体は、1以上の一時的でない、有形のコンピュータ読み取り可能な記録媒体の担持構造を包含する。例示として限定されるものではないが、コンピュータ読み取り可能な記憶媒体は、必要に応じて、たとえばFPGAFieldProgrammableGateArray又はASICApplicationSpecificICのような半導体に基づいた又は他の集積回路IC、ハードディスク、HDD、HHDHybridHardDrive、光ディスク、ODDOpticalDiscDrive、光磁気ディスク、光磁気ドライブ、フロプティカルディスク、フロプティカルディスクドライブFDD、磁気テープ、ホログラフィック記憶媒体、SSDSolidStateDrive、RAMドライブ、SECUREDIGITALカード、SECUREDIGITALドライブ、または別の適切なコンピュータ読み取り可能な記憶媒体、或いはこれらの2以上の組み合わせを含む場合がある。ここで、コンピュータ読み取り可能な記憶媒体に対する言及は、35USC§101の下での特許の保護のために適格でない媒体を排除する。ここで、コンピュータ読み取り可能な記憶媒体に対する言及は、35USC§101の下での特許の保護のために適格でないという点で、いわば伝搬する電気又は電磁信号のような信号伝達の一時的な形態を排除する。本発明の開示は、適切な記憶を実現する1以上のコンピュータ読み取り可能な記憶媒体を含んでいる。特定の実施の形態では、コンピュータ読み取り可能な記憶媒体は、必要に応じて、たとえば1以上の内部レジスタ又はキャッシュのような1以上のプロセッサ1302の部分、1以上のメモリ1304の部分、1以上のストレージ1306の部分、又はこれらの組み合わせを実現する。特定の実施の形態では、コンピュータ読み取り可能な記憶媒体は、RAM又はROMを実現する。特定の実施の形態では、コンピュータ読み取り可能な記憶媒体は、揮発性又は持続性のメモリを実現する。特定の実施の形態では、1以上のコンピュータ読み取り可能な記憶媒体は、ソフトウェアを統合する。ここで、ソフトウェアに対する言及は、1以上のアプリケーション、バイトコード、1以上のコンピュータプログラム、1以上の実行ファイル、1以上の命令、ロジック、マシンコード、1以上のスクリプト、又はソースコードを包含する場合があり、逆に、これら1以上のアプリケーション、バイトコード、1以上のコンピュータプログラム、1以上の実行ファイル、1以上の命令、ロジック、マシンコード、1以上のスクリプト、又はソースコードがソフトウェアを示す場合がある。特定の実施の形態では、ソフトウェアは、1以上のアプリケーションプログラミングインタフェースAPIを含む。この開示は、適切なプログラミング言語又はプログラミング言語の組み合わせで書かれるか又は表現される適切なソフトウェアを含む。特定の実施の形態では、ソフトウェアは、ソースコード又はオブジェクトコードとして表現される。特定の実施の形態では、ソフトウェアは、たとえばC,Perlのような高水準プログラミング言語、又はその適切な拡張で表現される。特定の実施の形態では、ソフトウェアは、アセンブリ言語又はマシンコードのような低水準プログラミング言語で表現される。特定の実施の形態では、ソフトウェアは、JAVAで表現される。特定の実施の形態では、ソフトウェアは、HTMLHyperTextMarkupLanguage、XMLExtensibleMarkupLanguage又は他の適切なマークアップ言語で表現される。本発明の開示は、当業者が理解することができる例示的な実施の形態に対する全ての変形、置換、変更を包含するものである。同様に、必要に応じて、特許請求の範囲は、当業者が理解する例示的な実施の形態に対する全ての変形、置換及び変更を包含する。以下、本願発明の特徴を付記として示す。付記11以上のコンピュータ装置により、ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、を含むことを特徴とする方法。付記2前記1以上の数値の変数は、1以上の入力の数値の変数と1以上の中間の数値の変数とを含み、前記1以上の文字列の変数は、1以上の入力の文字列の変数と1以上の中間の文字列の変数とを含み、前記1以上の入力の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の入力の文字列の変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの仕様に基づいて決定され、前記1以上の中間の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の中間の文字列に変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの記号的実行を行うことで決定される、付記1記載の方法。付記3前記第二の数値に関する制約は、前記第一の文字列に関する制約と前記第二の演算とに基づいて推定され、前記第二の文字列に関する制約は、前記第一の数値に関する制約と前記第一の演算とに基づいて推定される、付記1記載の方法。付記4前記第二の数値に関する制約と前記第二の文字列に関する制約は、ソフトウェアモジュールを実現するプログラミング言語と、前記ソフトウェアモジュールが実行されるランタイム環境との仕様に基づいて更に推定される、付記3記載の方法。付記5全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満たす解を発見することを試みるステップは、前記1以上の数値の変数と前記1以上の文字列の変数とについて異なる可能性のある値を繰返し試み、ある解が発見されるか、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とが満たされないと判定されるか、又はある繰り返し回数が閾値に到達するまで、前記異なる可能性のある値が前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約の全てを満たす解を生成するかを検査するステップと、前記解が発見された場合、前記1以上の数値の変数と前記1以上の文字列の変数の値を出力するステップと、を含む付記1記載の方法。付記6前記ソフトウェアモジュールは、1以上の条件分岐点と前記1以上の条件分岐点から得られる前記1以上の実行経路とを含み、前記1以上の条件分岐点のそれぞれは、前記1以上の数値の変数と前記1以上の文字列の変数とにより特定される分岐条件に関連され、前記ソフトウェアモジュールの実行の間、前記1以上の条件分岐点のそれぞれで、前記ソフトウェアモジュールは、前記1以上の条件分岐点に関連する分岐条件が満たされるかに依存して、前記1以上の実行経路のうちの実行経路に進む、付記1記載の方法。付記7前記可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、前記ソフトウェアモジュールの前記1以上の数値の変数と前記1以上の文字列の変数のうちの特定の変数に適用される1以上の制約のセットを決定するステップと、それぞれの制約のセットは、前記ソフトウェアモジュールの前記1以上の実行経路のうちの特定の実行経路に対応し、前記制約が満たされた場合、前記ソフトウェアモジュールに対応する実行経路の終わりに到達させ、前記それぞれの制約のセットを満たす1以上の解を発見するステップと、前記解に基づいて前記ソフトウェアモジュールについて1以上のテスト入力値のセットを生成するステップと、それぞれのテスト入力値のセットを前記ソフトウェアモジュールに適用することで、増加されるテスト範囲で前記ソフトウェアモジュールを検査するステップと、を含む付記6記載の方法。付記8前記それぞれの制約のセットは、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とに基づいて決定される、付記7記載の方法。付記9前記可能性のある値について前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールに記号的実行を行い、制約のセットを取得するステップを更に含む、付記7記載の方法。付記101以上のプロセッサにより実行可能な命令を含むメモリと、前記メモリに結合され、前記命令を実行する1以上のプロセッサとを備えるシステムであって、前記1以上のプロセッサは、前記命令を実行したときに、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうちの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を有するソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、実行することを特徴とするシステム。付記11前記1以上の数値の変数は、1以上の入力の数値の変数と1以上の中間の数値の変数とを含み、前記1以上の文字列の変数は、1以上の入力の文字列の変数と1以上の中間の文字列の変数とを含み、前記1以上の入力の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の入力の文字列の変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの仕様に基づいて決定され、前記1以上の中間の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の中間の文字列に変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの記号的実行を行うことで決定される、付記10記載のシステム。付記12前記第二の数値に関する制約は、前記第一の文字列に関する制約と前記第二の演算とに基づいて推定され、前記第二の文字列に関する制約は、前記第一の数値に関する制約と前記第一の演算とに基づいて推定される、付記10記載のシステム。付記13前記第二の数値に関する制約と前記第二の文字列に関する制約は、ソフトウェアモジュールを実現するプログラミング言語と、前記ソフトウェアモジュールが実行されるランタイム環境との仕様に基づいて更に推定される、付記12記載のシステム。付記14全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満たす解を発見することを試みるステップは、前記1以上の数値の変数と前記1以上の文字列の変数とについて異なる可能性のある値を繰返し試み、ある解が発見されるか、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とが満たされないと判定されるか、又はある繰り返し回数が閾値に到達するまで、前記異なる可能性のある値が前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約の全てを満たす解を生成するかを検査するステップと、前記解が発見された場合、前記1以上の数値の変数と前記1以上の文字列の変数の値を出力するステップと、を含む付記10記載のシステム。付記15前記ソフトウェアモジュールは、1以上の条件分岐点と前記1以上の条件分岐点から得られる前記1以上の実行経路とを含み、前記1以上の条件分岐点のそれぞれは、前記1以上の数値の変数と前記1以上の文字列の変数とにより特定される分岐条件に関連され、前記ソフトウェアモジュールの実行の間、前記1以上の条件分岐点のそれぞれで、前記ソフトウェアモジュールは、前記1以上の条件分岐点に関連する分岐条件が満たされるかに依存して、前記1以上の実行経路のうちの実行経路に進む、付記10記載のシステム。付記16前記可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールの前記1以上の数値の変数と前記1以上の文字列の変数のうちの特定の変数に適用される1以上の制約のセットを決定するステップと、それぞれの制約のセットは、前記ソフトウェアモジュールの前記1以上の実行経路のうちの特定の実行経路に対応し、前記制約が満たされた場合、前記ソフトウェアモジュールに、対応する実行経路の終わりに到達させ、前記それぞれの制約のセットを満たす1以上の解を発見するステップと、前記解に基づいて前記ソフトウェアモジュールについて1以上のテスト入力値のセットを生成するステップと、それぞれのテスト入力値のセットを前記ソフトウェアモジュールに適用することで、増加されるテスト範囲で前記ソフトウェアモジュールを検査するステップと、を含む付記15記載のシステム。付記17前記それぞれの制約のセットは、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とに基づいて決定される、付記16記載のシステム。付記18前記可能性のある値について前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールに記号的実行を行い、制約のセットを取得するステップを更に含む、付記16記載のシステム。付記191以上のコンピュータ装置に、ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析するステップと、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定するステップと、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定するステップと、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現するステップと、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現するステップと、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、を実行させる命令を含むプログラムを記録したコンピュータ読み取り可能な記録媒体。付記20前記1以上の数値の変数は、1以上の入力の数値の変数と1以上の中間の数値の変数とを含み、前記1以上の文字列の変数は、1以上の入力の文字列の変数と1以上の中間の文字列の変数とを含み、前記1以上の入力の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の入力の文字列の変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの仕様に基づいて決定され、前記1以上の中間の数値の変数のうちの特定の変数に適用される前記第一の数値に関する制約と、前記1以上の中間の文字列に変数のうちの特定の変数に適用される前記第一の文字列に関する制約とは、前記ソフトウェアモジュールの記号的実行を行うことで決定される、付記19記載のコンピュータ読み取り可能な記録媒体。付記21前記第二の数値に関する制約は、前記第一の文字列に関する制約と前記第二の演算とに基づいて推定され、前記第二の文字列に関する制約は、前記第一の数値に関する制約と前記第一の演算とに基づいて推定される、付記19記載のコンピュータ読み取り可能な記録媒体。付記22前記第二の数値に関する制約と前記第二の文字列に関する制約は、ソフトウェアモジュールを実現するプログラミング言語と、前記ソフトウェアモジュールが実行されるランタイム環境との仕様に基づいて更に推定される、付記21記載のコンピュータ読み取り可能な記録媒体。付記23全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満たす解を発見することを試みるステップは、前記1以上の数値の変数と前記1以上の文字列の変数とについて異なる可能性のある値を繰返し試み、ある解が発見されるか、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とが満たされないと判定されるか、又はある繰り返し回数が閾値に到達するまで、前記異なる可能性のある値が前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約の全てを満たす解を生成するかを検査するステップと、前記解が発見された場合、前記1以上の数値の変数と前記1以上の文字列の変数の値を出力するステップと、を含む付記19記載のコンピュータ読み取り可能な記録媒体。付記24前記ソフトウェアモジュールは、1以上の条件分岐点と前記1以上の条件分岐点から得られる前記1以上の実行経路とを含み、前記1以上の条件分岐点のそれぞれは、前記1以上の数値の変数と前記1以上の文字列の変数とにより特定される分岐条件に関連され、前記ソフトウェアモジュールの実行の間、前記1以上の条件分岐点のそれぞれで、前記ソフトウェアモジュールは、前記1以上の条件分岐点に関連する分岐条件が満たされるかに依存して、前記1以上の実行経路のうちの実行経路に進む、付記19記載のコンピュータ読み取り可能な記録媒体。付記25前記可能性のあるエラーについて前記ソフトウェアモジュールを検査するステップと、前記ソフトウェアモジュールの前記1以上の数値の変数と前記1以上の文字列の変数のうちの特定の変数に適用される1以上の制約のセットを決定するステップと、それぞれの制約のセットは、前記ソフトウェアモジュールの前記1以上の実行経路のうちの特定の実行経路に対応し、前記制約が満たされた場合、前記ソフトウェアモジュールに対応する実行経路の終わりに到達させ、前記それぞれの制約のセットを満たす1以上の解を発見するステップと、前記解に基づいて前記ソフトウェアモジュールについて1以上のテスト入力値のセットを生成するステップと、それぞれのテスト入力値のセットを前記ソフトウェアモジュールに適用することで、増加されるテスト範囲で前記ソフトウェアモジュールを検査するステップと、を含む付記24記載のコンピュータ読み取り可能な記録媒体。付記26前記それぞれの制約のセットは、前記第一及び第二の数値に関する制約と前記第一及び第二の文字列に関する制約とに基づいて決定される、付記25記載のコンピュータ読み取り可能な記録媒体。付記27前記可能性のある値について前記ソフトウェアモジュールを検査するステップは、前記ソフトウェアモジュールに記号的実行を行い、制約のセットを取得するステップを更に含む、付記25記載のコンピュータ読み取り可能な記録媒体。付記28ソフトウェアモジュールに関連する1以上の第一の数値に関する制約と1以上の第一の文字列に関する制約とを分析する手段と、前記ソフトウェアモジュールは、1以上の数値の変数、1以上の文字列の変数、前記1以上の数値の変数のうちの特定の変数に適用され、数値又は文字列に関する結果を生成1以上の第一の演算、及び前記1以上の文字列の変数のうつの特定の変数に適用され、数値又は文字列の変数を生成する1以上の第二の演算を備え、前記第一の数値に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記第一の文字列に関する制約は、前記1以上の数値の変数のうちの特定の変数に適用され、前記1以上の文字列の変数のうちの特定の変数に適用される1以上の第二の数値に関する制約を推定する手段と、前記1以上の数値の変数のうちの特定の変数に適用される1以上の第二の文字列に関する制約を推定する手段と、前記第一の数値に関する制約と前記第二の数値に関する制約のそれぞれを式で表現する手段と、前記第一の文字列に関する制約と前記第二の文字列に関する制約のそれぞれを有限状態マシンで表現する手段と、全ての前記第一及び第二の数値に関する制約と全ての前記第一及び第二の文字列に関する制約とを満足する前記1以上の数値の変数と前記1以上の文字列の変数とのうちの特定の変数の1以上の値を含む解を発見することを試みることで、1以上の可能性のあるエラーについて前記ソフトウェアモジュールを検査する手段と、を備えることを特徴とするシステム。"