文献

J-GLOBAL ID：201202208908683800   整理番号：12A1206611

組込みソフトウェアのアセンブラのSMT検証

Verification of embedded software in Assembly code by SMT prover

著者 (3件)： 竹下淳 (金沢大 大学院自然科学研究科) ,  小橋潤平 (金沢大) ,  山根智 (金沢大)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 112  号： 116(MSS2012 1-29)  ページ： 37-42  発行年： 2012年06月25日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿では,組込みアセンブリプログラムを対象としたSMT有界モデル検査手法を以下のように提案する。(1)検証の前処理として,アセンブリプログラムをSSA形式に変換処理する。(2)アセンブリプログラムのSSA形式からSMT-LIBに変換してSMT有界モデル検査を行う。以上の検証手法をJavaで実装して実証実験を行った。(著者抄録)

シソーラス用語： *充足可能性問題 ,  理論 ,  検証 ,  埋込み【挿入】 ,  アセンブラ ,  *モデル検査 ,  Java ,  実証実験
準シソーラス用語： *組込みソフトウェア

分類 (2件)： 品質検査  (KB04020L) ,  計算機ソフトウエア一般  (JD01010K)

タイトルに関連する用語 (4件)： 組込みソフトウェア ,  アセンブラ ,  SMT ,  検証