| 講演名 | 2014/1/23 CISC型組込みアセンブリプログラムのSMTベースの有界モデル検査 竹下 淳, 小橋 潤平, 山根 智, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本研究では,組込みシステム向けアセンブリプログラムのコードブロックを対象とした,SMT有界モデル検査手法による性質検証を述べる.アセンブリプログラムのコードブロック生成規則とモデル化について提案する.また,実際のプログラムに対して提案手法によるコード変換を行った. |
| 抄録(英) | In this paper, we describe the method of verification by bounded model checking based in SMT using Code Block for embedded system assembly program. We propose the rule of Code Block generation, and method of modelling this block data. Finally we will verify actual programs. |
| キーワード(和) | SMTソルバ / 有界モデル検査 / 組込みシステム / アセンブリプログラム / 形式検証 |
| キーワード(英) | SMT solver / Bounded Model Checking / Embedded System / Assembly Program / Formal Verification |
| 資料番号 | SS2013-59,MSS2013-62 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2014/1/23(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | CISC型組込みアセンブリプログラムのSMTベースの有界モデル検査 |
| サブタイトル（和） | |
| タイトル（英） | Bounded model checking based in SMT for CISC embedded assembly programs |
| サブタイトル（和） | |
| キーワード(1)（和/英） | SMTソルバ / SMT solver |
| キーワード(2)（和/英） | 有界モデル検査 / Bounded Model Checking |
| キーワード(3)（和/英） | 組込みシステム / Embedded System |
| キーワード(4)（和/英） | アセンブリプログラム / Assembly Program |
| キーワード(5)（和/英） | 形式検証 / Formal Verification |
| 第 1 著者 氏名（和/英） | 竹下 淳 / Atsushi TAKESHITA |
| 第 1 著者 所属（和/英） | 金沢大学大学院自然科学研究科 Graduate School of Natural Science and Technology, Kanazawa University |
| 第 2 著者 氏名（和/英） | 小橋 潤平 / Junpei KOBASHI |
| 第 2 著者 所属（和/英） | 金沢大学大学院自然科学研究科 Graduate School of Natural Science and Technology, Kanazawa University |
| 第 3 著者 氏名（和/英） | 山根 智 / Satoshi YAMANE |
| 第 3 著者 所属（和/英） | 金沢大学理工学域電子情報学類 School of Science and Engineering, Kanazawa Univer-sity |
| 発表年月日 | 2014/1/23 |
| 資料番号 | SS2013-59,MSS2013-62 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | 422 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |