本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。