モデル検査技術を利用したプログラム解析器の生成ツール

• Item type: Trans(1)
• 公開日: 2003-10-15
• タイトル: モデル検査技術を利用したプログラム解析器の生成ツール
• タイトル / 言語: en
• タイトル: Generation of Program Analyzer Based on Model Checking
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 東京大学大学院情報理工学系研究科
• 著者所属: 東京大学大学院情報理工学系研究科／科学技術振興事業団
• 著者所属: 東京大学大学院情報理工学系研究科
• 著者所属: 東京大学大学院情報理工学系研究科／科学技術振興事業団
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo/Japan Science and Technology Corporation
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Technology, The University of Tokyo/Japan Science and Technology Corporation
• 著者名: 山岡, 裕司; 胡振江; 武市, 正人; 小川, 瑞史
• 著者名(英): Yuji, Yamaoka; Zhenjiang, Hu; Masato, Takeichi; Mizuhiro, Ogawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，時相論理式によって仕様が記述されたプログラム解析をモデル検査技術の利用によって行うツールについて述べる．本ツールは，対象プログラム言語はJimple，プログラム解析の仕様記述言語は時相論理CTL-FVである．JimpleはJavaと相互変換可能な3番地コードからなる中間言語であり，Javaに比べプログラム解析や最適化が適用しやすい．また，CTL-FVはCTL（ComputationTree Logic）を拡張した時相論理であり，プログラム中の情報を述語に引用することを許したところに大きな特徴がある．CTL-FV によって多くのプログラム解析が記述できるため，本ツールを使用するとJimpleプログラムに対し様々な解析を自動的に行うことができるようになる．今回，モデル検査を既存のモデル検査ツールSMVをそのまま利用することによって実装が非常に簡単になり，Java言語で約500行（コメント除く）のプログラムでこれが実現できた．また，標準ライブラリのいくつかのクラスに対して無用命令の検出を本ツールにより実行したところ，比較的大きなサイズのクラスに対しても数分で解析することができた．ここでは，主に本ツールの設計と実装について説明する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we describe a tool that automatically performs program analysis using modelchecking techniques. The tool has two characteristics; the target program is Jimple, and the specification of program analysis is described in temporal logic CTL-FV. Jimple is mutually convertible with Java; it is a 3-address intermediate language and is easier to perform program analyses and optimizations than Java. CTL-FV is an extension of CTL (Computation Tree Logic) to allow quoting information in a program to formulas. CTL-FV can describe man program analyses, thus our tool can carry out various analyses automatically. By the use of the well-developed model-checker SMV, we implemented this tool with only 500 lines of code in Java. As an example, dead code detection is performed to some classes in the standard library, and relatively large classes can be analyzed in a few minutes. We explain the design and the implementation of the tool.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 44, 号 SIG13(PRO18), p. 25-37, 発行日 2003-10-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会