SAT技術の進化と応用 〜パズルからプログラム検証まで〜：7. SMTソルバーによるプログラム検証

情報処理学会 Web Site

書誌事項

タイトル別名
  • SMTソルバーによるプログラム検証
  • SMT ソルバー ニ ヨル プログラム ケンショウ
  • SAT Evolution and Applications：7. Program Verification Using SMT Solvers

この論文をさがす

抄録

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

収録刊行物

  • 情報処理

    情報処理 57 (8), 734-737, 2016-07-15

    東京 : 情報処理学会 ; 1960-

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ