近年，人命や財産に関わるようなシステムがソフトウェアで制御されるようになっている．そのため，これらのソフトウェアが安全に動作することを何らかの手段で保証することが必要である．ソフトウェアの検証の有効な手法としてモデル検査が脚光を浴びているが，現在の主流は有限状態のモデル検査であり，関数型プログラミングで用いられる高階関数などの機能を使ったプログラムをうまく検証することができない．本講演では高階関数型プログラムを検証対象とする高階ソフトウェアモデル検査を紹介する．まず，高階ソフトウェアモデル検査の基本的な実現方法を説明し，次に，検証対象を広げるための様々な拡張手法について述べる．最後に，モデル検査を含む全自動検証手法全体の今後の展望について述べる．