| 講演名 | 2012-07-02 組込みソフトウェアのアセンブラのSMT検証(システムと信号処理及び一般) 竹下 淳, 小橋 潤平, 山根 智, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,組込みアセンブリプログラムを対象としたSMT有界モデル検査手法を以下のように提案する.(1)検証の前処理として,アセンブリプログラムをSSA形式に変換処理する.(2)アセンブリプログラムのSSA形式からSMT-LIBに変換してSMT有界モデル検査を行う.以上の検証手法をJavaで実装して実証実験を行った. |
| 抄録(英) | We propose the technique of Bounded Model Checking(BMC) for embedded assembly program. We use SMT solver for BMC. We also propose improvement of SSA conversion algorithm for assembly program and implement the Algorithm using Java language. Finally, we verify the simple assembly program's property of a real embedded robot system. |
| キーワード(和) | SMTソルバー / 有界モデル検査 / 静的単一代入(SSA) / 組込みアセンブリプログラム |
| キーワード(英) | SMT solver / Bounded Model Checking / Single Static Assignment(SSA) / embedded assembly program |
| 資料番号 | CAS2012-7,VLD2012-17,SIP2012-39,MSS2012-7 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2012/6/25(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 組込みソフトウェアのアセンブラのSMT検証(システムと信号処理及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Verification of embedded software in Assembly code by SMT prover |
| サブタイトル（和） | |
| キーワード(1)（和/英） | SMTソルバー / SMT solver |
| キーワード(2)（和/英） | 有界モデル検査 / Bounded Model Checking |
| キーワード(3)（和/英） | 静的単一代入(SSA) / Single Static Assignment(SSA) |
| キーワード(4)（和/英） | 組込みアセンブリプログラム / embedded assembly program |
| 第 1 著者 氏名（和/英） | 竹下 淳 / Atsushi TAKESHITA |
| 第 1 著者 所属（和/英） | 金沢大学大学院自然科学研究科 Graduate School of Natural Science and Technology, Kanazawa University |
| 第 2 著者 氏名（和/英） | 小橋 潤平 / Junpei KOBASHI |
| 第 2 著者 所属（和/英） | 金沢大学理工学域電子情報学類 Division of Electrical and Computer Engineering, Kanazawa University |
| 第 3 著者 氏名（和/英） | 山根 智 / Satoshi YAMANE |
| 第 3 著者 所属（和/英） | 金沢大学理工学域電子情報学類 Division of Electrical and Computer Engineering, Kanazawa University |
| 発表年月日 | 2012-07-02 |
| 資料番号 | CAS2012-7,VLD2012-17,SIP2012-39,MSS2012-7 |
| 巻番号（vol） | vol.112 |
| 号番号（no） | 114 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |