著者

徳本 晋 上原 忠弘 宗像 一樹 菊地 英幸 江口 亨 石田 晴幸 馬場 匡史

雑誌

組込みシステムシンポジウム2011論文集

巻号頁・発行日

vol.2011, pp.23-1-23-8, 2011-10-12

---

KLEE は LLVM 中間コードを対象としてシンボリック実行をすることができるツールである.C/C++ で書かれたプログラムは llvm-gcc や clang などのコンパイラで LLVM ビットコードにコンパイルできるため,C/C++ プログラムの検証ツールとして KLEE は期待されている.今回,2 つのプログラムについて KLEE を適用し,それにより検出したバグとその特徴を紹介するとともに,KLEE のバグ検出能力について考察する.また,他の商用 C/C++ 検証ツールで対象プログラムを解析したときの結果と,KLEE を使った場合との比較について報告する.さらに KLEE 適用時の課題を解決すべく,KLEE で生成したテストケースを CPPUNIT のテストコードへ変換するツールについても報告する.