講演名 2012-11-22
アセンブリプログラムに対するSMTソルバを使用する有界モデル検査
小橋 潤平, 竹下 淳, 山根 智,
PDFダウンロードページ PDFダウンロードページへ
抄録(和) 本稿では,組み込みシステム向けアセンブリ言語プログラムコードのレジスタレベルモデルに対して,SMTソルバを用いた有界モデル検査手法による性質検証を述べる.SMTソルバを用いた検証手法とアセンブリコードのモデル化について提案し,簡単なアセンブリプログラムに対して提案した手法による性質検証を行なった.
抄録(英) In this paper, we state property verification by Bounded Model Checking using SMT solver for register level model of assembly program code for embedded system. We propose verifying by SMT solver and modeling for assembly code to predicate logic formula, and we experimented on our method for simple assembly program.
キーワード(和) SMTソルバ / 有界モデル検査 / 組み込みシステム / アセンブリプログラム / 形式検証
キーワード(英) SMT solver / Bounded Model Checking / Embedded system / Assembly program / Systematic verification
資料番号 KBSE2012-41
発行日

研究会情報
研究会 KBSE
開催期間 2012/11/15(から1日開催)
開催地(和)
開催地(英)
テーマ(和)
テーマ(英)
委員長氏名(和)
委員長氏名(英)
副委員長氏名(和)
副委員長氏名(英)
幹事氏名(和)
幹事氏名(英)
幹事補佐氏名(和)
幹事補佐氏名(英)

講演論文情報詳細
申込み研究会 Knowledge-Based Software Engineering (KBSE)
本文の言語 JPN
タイトル(和) アセンブリプログラムに対するSMTソルバを使用する有界モデル検査
サブタイトル(和)
タイトル(英) SMT-based Bounded Model Checking for Assembly program
サブタイトル(和)
キーワード(1)(和/英) SMTソルバ / SMT solver
キーワード(2)(和/英) 有界モデル検査 / Bounded Model Checking
キーワード(3)(和/英) 組み込みシステム / Embedded system
キーワード(4)(和/英) アセンブリプログラム / Assembly program
キーワード(5)(和/英) 形式検証 / Systematic verification
第 1 著者 氏名(和/英) 小橋 潤平 / Jumpei KOBASHI
第 1 著者 所属(和/英) 金沢大学理工学域電子情報学類
School of Science and Engineering, Kanazawa Univer-sity
第 2 著者 氏名(和/英) 竹下 淳 / Atsushi TAKESHITA
第 2 著者 所属(和/英) 金沢大学大学院自然科学研究科
Graduate School of Natural Science and Technology , Kanazawa University
第 3 著者 氏名(和/英) 山根 智 / Satoshi YAMANE
第 3 著者 所属(和/英) 金沢大学理工学域電子情報学類
School of Science and Engineering, Kanazawa Univer-sity
発表年月日 2012-11-22
資料番号 KBSE2012-41
巻番号(vol) vol.112
号番号(no) 314
ページ範囲 pp.-
ページ数 6
発行日