しかし、大規模論理回路の処理には状態数の爆発問題が伴なう。 実設計の状態数は非常に大きいので限られた時間と記憶量で 近年の設計の検証を行なうことは非常に困難である。
二分モーメントグラフ(BMD：Binary Moment Diagram)と 二分決定グラフ(BDD：Binary Decision Diagram)に基づいて記号表現 を導入し検証する手法が用いられるようになり、 これらの手法により状態の直接的な表現に基づいた技術では扱えないような 複雑なシステムも検証可能になってきた。 これらの手法でのデータ構造は状態の効率的な表現を用いている。 それによって演算は、状態一つずつに対してではなく、状態の集合に対して行われる。 しかし, 記号表現を用いてもなお状態の爆発の可能性がある。
本修士論文では、ハードウェア検証のために検査する状態集合を縮小するための 二つの処理手法を示す。 一番目の手法は、 Verilog HDL ソースから抽象化した状態空間を自動的に抽出するための 形式的検証のための抽象解釈を自動適用するための アルゴリズムである。 この手法により、モデル検査において自動的に抽象解釈を適用することができる。 二番目の手法は、 二分モーメントグラフを用いた大規模多項式の操作のための新しい手法である。 この手法は、ゼロサプレス型二分決定グラフ(ZBDD：Zero-suppressed BDD)を用いた以前の手法より効率が よいことが実験により示された。