プログラムの仕様記述，スケジューリングなど多くの応用問題は，命題論理で記述するよりも，整数の算術式や配列演算子など問題固有の記号を命題論理に埋め込んだ述語論理を用いたほうが記述しやすい．SMT（satis ability modulo theories）は，述語論理の充足可能性判定をSATソルバーと理論ソルバーを連携させて行うための技術である．本稿では，最近のSMTソルバーで用いられている求解技術を概観するとともに，応用事例として，SMTソルバーを利用して仕様付きプログラムの正当性を自動検証するプログラム検証技術を紹介する．