検証対象とする回路の厳密プロパティ検査を目的とし，論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を継続している．定理証明は回路構造と接続の正当性に関するプロパティ検査に専念する．実規模での組合せ回路全体での振る舞い検証は，並列化モデルチェッカを用いて検証することになるが，スケーラブルでかつ繰り返し構造を有するPEの実例として，高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し，Mizarプルーフチェッカを用いた機械検証を行ったところ，回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に既に成功している．
現在，関数型言語系の上のハードウェアコンパイラを機能拡張する目的のため，開発中の Melasy+ ハードウェアコンパイラについて，各演算機能に相当するLOTOSライブラリを機能拡張する研究を実施している．具体的には，高位設計としての対象回路の構成情報として，観測レベル，振る舞いレベル，ゲートレベルの3種のライブラリとしてレベル別設計を行い，各々のレベル間での相互検証を可能とした．
更に，LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ，状態空間生成器を用いて初期状態から駆動するが，状態空間生成時の既生成マーキングを記憶するハッシュメモリの効率化を図るため，削除可能状態のオンライン判定アルゴリズムに関する検討を行った．なおペトリネット検証系に関する基礎研究として，サブマーキング法を用いた状態空間の抽象化と準ホーム状態の存在検知，一般ペトリネットのSATソルバーを用いた構造解析による強L3活性構造の検知などに関する成果を得た．