本講義では、高階モデル検査とその応用に関する最新の話題を通して、計算モ デルや形式言語、オートマトンなどに関する理論がソフトウェアの信頼性向上 などの現実的に重要な課題の解決にどう役立つのかを解説する。モデル検査は システム検証手法として広く応用されるようになってきているが、高階モデル 検査問題は従来のモデル検査問題の拡張で、高階再帰スキームと呼ばれる高階 の木生成文法によって生成される無限木の性質を検査する問題である。最近に なって、高階関数型プログラムの検証問題との密接なつながりが発見されたこ とや、効率の良いアルゴリズムが発見されたことなどから注目を集め、プログ ラム検証への応用が急速に進みつつある。この講義では、高階モデル検査問題 の定義とアルゴリズム、プログラム検証への応用などについて概観する。