Bibliographic Information
- Other Title
-
- SAT技術の進化と応用 〜パズルからプログラム検証まで〜:7. SMTソルバーによるプログラム検証
- SMT ソルバー ニ ヨル プログラム ケンショウ
- SAT Evolution and Applications:7. Program Verification Using SMT Solvers
Search this article
Abstract
プログラムの仕様記述,スケジューリングなど多くの応用問題は,命題論理で記述するよりも,整数の算術式や配列演算子など問題固有の記号を命題論理に埋め込んだ述語論理を用いたほうが記述しやすい.SMT(satis ability modulo theories)は,述語論理の充足可能性判定をSATソルバーと理論ソルバーを連携させて行うための技術である.本稿では,最近のSMTソルバーで用いられている求解技術を概観するとともに,応用事例として,SMTソルバーを利用して仕様付きプログラムの正当性を自動検証するプログラム検証技術を紹介する.
Journal
-
- 情報処理
-
情報処理 57 (8), 734-737, 2016-07-15
東京 : 情報処理学会 ; 1960-
- Tweet
Keywords
Details 詳細情報について
-
- CRID
- 1050001337907133696
-
- NII Article ID
- 40020914132
-
- NII Book ID
- AN00116625
-
- ISSN
- 04478053
-
- NDL BIB ID
- 027555386
-
- Text Lang
- ja
-
- Article Type
- departmental bulletin paper
-
- Data Source
-
- IRDB
- NDL
- CiNii Articles