文献

J-GLOBAL ID：201002204714123570   整理番号：10A1001158

SATソルバ・SMTソルバの技術と応用

SAT/SMT solvers and their applications

著者 (1件)： 梅村晃広 ((株)NTTデータ)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 27  号： 3  ページ： 3.24-3.35 (J-STAGE)  発行年： 2010年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本解説記事では,各種フォーマルメソッドの背後で動作する証明(補助)エンジンとしても注目を集めている,SATソルバ,SMTソルバについて,その背景,基本的な概念,技術動向および応用についての動向を解説する.SATソルバは近年飛躍的な技術革新があり,これに伴ない,いろいろな分野から応用への注目が集まるようになった.また,これに合わせるようにSMTソルバという発展的な概念も発生してきた.本稿は,これらについて,特にフォーマルメソッドとの関係における位置付けを概説するものである.(著者抄録)

シソーラス用語： *形式的手法【計算機】 ,  定理証明 ,  *モデル検査 ,  計算機システム開発 ,  応用プログラム ,  プログラム解析 ,  *充足可能性問題 ,  述語論理 ,  計算機アルゴリズム ,  状態遷移図 ,  命題論理 ,  ソルバ ,  静的コード解析
準シソーラス用語： 静的解析

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (26件)：

• BARRETT, C. Satisfiability Modulo Theories. Handbook of Satisfiability. 2009, 825-885
• BIERE, A. Symbolic Model Checking without BDDs. Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99). 1999, 193-207
• BIERE, A. eds. Handbook of Satisfiability. 2009
• BORGER, E. The Classical Decision Problem. 1997
• BRADLEY, A. R. The Calculus of Computation : Decision Procedures with Applications to Verification. 2007

タイトルに関連する用語 (4件)： SAT ,  ソルバ ,  SMT ,  応用