文献

J-GLOBAL ID：201302259447686790   整理番号：13A0026444

アセンブリプログラムに対するSMTソルバを使用する有界モデル検査

SMT-based Bounded Model Checking for Assembly program

著者 (3件)： 小橋潤平 (金沢大 理工学域) ,  竹下淳 (金沢大 大学院自然科学研究科) ,  山根智 (金沢大 理工学域)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 112  号： 314(KBSE2012 38-57)  ページ： 19-24  発行年： 2012年11月15日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿では,組み込みシステム向けアセンブリ言語プログラムコードのレジスタレベルモデルに対して,SMTソルバを用いた有界モデル検査手法による性質検証を述べる。SMTソルバを用いた検証手法とアセンブリコードのモデル化について提案し,簡単なアセンブリプログラムに対して提案した手法による性質検証を行なった。(著者抄録)

シソーラス用語： *アセンブリ言語 ,  充足可能性問題 ,  応用プログラム ,  システム ,  限界 ,  *モデル検査 ,  検証 ,  *レジスタ ,  組込みシステム
準シソーラス用語： ソルバ ,  形式検証 ,  有界

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

引用文献 (16件)：

• SCHLICH, B. Model Checking Checking of Software for Microcon-trollers. ACM Transactions on Embedded Computing Sys-tems. 2010, 9, 4, 1-27
• 高井利憲. アセンブラプログラムのモデル検査によるバグ解析事例. 第四回システム検証の科学技術シンポジウム講演論文集. 2007, 65-70
• 水口大知. 組み込みソフトウェア開発におけるモデル検査の適用事例. コンピュータソフトウェア. 2005, 22, 1, 77-90
• CORDEIRO, L. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. Proceedings of the 2009 IEEE/ACM International Conference on Automated Soft-ware Engineering. 2009, 137-148
• 土屋達弘. 充足可能性判定を利用したモデル検査. 第7回プログラミングおよびプログラミング言語サマースクール. 2009

タイトルに関連する用語 (5件)： アセンブリ ,  SMT ,  ソルバ ,  有界 ,  モデル検査