）高階モデル検査とは、従来のモデル検査をより一般化、強力にしたものであり、正確には、「高階再帰スキーム」と 呼ばれる高階の木生成文法によって生成される無限木が与えられた性質（例えば「無限パスを持つか？」「aというラベルがついたノードの下にbというラベルが出現しうるか？」など）を検証する手法です。
そのような高階モデル検査が原理的に可能である（高階モデル検査問題が決定可能である）ことは 2006年にオックスフォード大学のOng教授によって証明されましたが、その最悪時間計算量が莫大（k階の高階再帰スキームの モデル検査はk重指数完全）であること、実際、Ong教授による決定可能性の証明で与えられているアルゴリズムが ほぼ常にk重指数時間かかるアルゴリズムであったことなどから、しばらくは理論家の間だけの興味の対象でした。
これに対し、2009年に小林が（１）一部のパラメタを固定すれば、高階モデル検査問題は、実は文法のサイズに対して 多項式時間で解けることを示すとともに、（２）典型的な入力に対しては効率よく動作する高階モデル検査を発見し、 さらに（３）多くの関数型プログラムの検証問題が高階モデル検査問題に帰着できることを示しました。 これによって、高階モデル検査問題はもはや理論家だけの興味の対象ではなく、応用への道が開けました。
下に述べるプログラム検証やデータ圧縮への本格的応用のためには、数千行、数万行規模の高階文法に対する モデル検査を行う必要がでてきます。そのために既に開発済みの高階モデル検査器を改良するとともに、 高階モデル検査の理論を整備して新しい高階モデル検査アルゴリズムを考案する研究を行っています。 これまでにTRecS, GTRecS, HorSatという３つのアルゴリズムを考案し、実装しています。 中でも最新のアルゴリズムHorSat2は現在(2018年)世界最速の高階モデル検査器で、 数千行規模の入力（入力によっては数十万行）に対しても動作しています。 上のリンクから高階モデル検査器を試すことができます。
上で述べたように、プログラム検証の問題を高階モデル検査問題に自動変換することによって プログラムの全自動検証を行うことができます。 これに基づいて 関数型言語OCaml用プログラム検証器MoCHiや 木構造処理プログラム検証器EHMTT Verifier を実装しました。
従来のソフトウェアモデル検査手法に対する高階モデル検査に基づくプログラム検証手法の利点は， 再帰や高階関数などのプログラムの制御構造を高階文法を用いることによって正確に表現・検証できることにあります。しかしながら， 検証対象のプログラムがオブジェクト指向プログラムや並行プログラムの場合，高階文法を用いても正確に制御構造を表現することが できません．そこで，高階文法に再帰型を加えてえられる「拡張高階モデル検査問題」を考え，その手続きおよびオブジェクト指向プログラムや並行プログラムの検証への応用に取り組んでいます．これに基づいて 関数オブジェクト指向言語Featherweight Java(FJ)用プログラム検証器などを実装しました．
高階モデル検査の対象である高階文法（あるいはラムダ計算）を用いると、大規模な木構造データをコンパクトに表現することができます。これによって超指数的圧縮率が得られる場合があり、Kolmogorov複雑性の理論によれば理論的には、(定数を除いて） 最適な圧縮サイズを実現することができます。しかも、高階モデル検査を用いることにより、 高階文法またはラムダ計算の項の形で圧縮したデータに対して、展開しないでパターン照合、置換などの操作を施すことができます。圧縮器の試作版はこちらで、 圧縮データに対する操作はこちらで 試すことができます。
問い合わせ先：小林（）