{"created":"2025-01-18T22:49:55.106507+00:00","updated":"2025-01-22T23:42:34.063894+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00016726","sets":["934:935:963:966"]},"path":["966"],"owner":"1","recid":"16726","title":["モデル検査技術を利用したプログラム解析器の生成ツール"],"pubdate":{"attribute_name":"公開日","attribute_value":"2003-10-15"},"_buckets":{"deposit":"08edc431-bb28-48d3-90f1-d18db41f5d2f"},"_deposit":{"id":"16726","pid":{"type":"depid","value":"16726","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"モデル検査技術を利用したプログラム解析器の生成ツール","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"モデル検査技術を利用したプログラム解析器の生成ツール"},{"subitem_title":"Generation of Program Analyzer Based on Model Checking","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"通常論文","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2003-10-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"東京大学大学院情報理工学系研究科"},{"subitem_text_value":"東京大学大学院情報理工学系研究科／科学技術振興事業団"},{"subitem_text_value":"東京大学大学院情報理工学系研究科"},{"subitem_text_value":"東京大学大学院情報理工学系研究科／科学技術振興事業団"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Graduate School of Information Science and Technology, The University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Graduate School of Information Science and Technology, The University of Tokyo/Japan Science and Technology Corporation","subitem_text_language":"en"},{"subitem_text_value":"Graduate School of Information Science and Technology, The University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Graduate School of Information Science and Technology, The University of Tokyo/Japan Science and Technology Corporation","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/16726/files/IPSJ-TPRO4413004.pdf"},"date":[{"dateType":"Available","dateValue":"2005-10-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO4413004.pdf","filesize":[{"value":"287.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"5b912e0b-06c3-4a71-8fe9-6c848f1e9b4d","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2003 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"山岡, 裕司"},{"creatorName":"胡振江"},{"creatorName":"武市, 正人"},{"creatorName":"小川, 瑞史"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Yuji, Yamaoka","creatorNameLang":"en"},{"creatorName":"Zhenjiang, Hu","creatorNameLang":"en"},{"creatorName":"Masato, Takeichi","creatorNameLang":"en"},{"creatorName":"Mizuhiro, Ogawa","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"本論文では，時相論理式によって仕様が記述されたプログラム解析をモデル検査技術の利用によって行うツールについて述べる．本ツールは，対象プログラム言語はJimple，プログラム解析の仕様記述言語は時相論理CTL-FVである．JimpleはJavaと相互変換可能な3番地コードからなる中間言語であり，Javaに比べプログラム解析や最適化が適用しやすい．また，CTL-FVはCTL（ComputationTree Logic）を拡張した時相論理であり，プログラム中の情報を述語に引用することを許したところに大きな特徴がある．CTL-FV によって多くのプログラム解析が記述できるため，本ツールを使用するとJimpleプログラムに対し様々な解析を自動的に行うことができるようになる．今回，モデル検査を既存のモデル検査ツールSMVをそのまま利用することによって実装が非常に簡単になり，Java言語で約500行（コメント除く）のプログラムでこれが実現できた．また，標準ライブラリのいくつかのクラスに対して無用命令の検出を本ツールにより実行したところ，比較的大きなサイズのクラスに対しても数分で解析することができた．ここでは，主に本ツールの設計と実装について説明する．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"37","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"25","bibliographicIssueDates":{"bibliographicIssueDate":"2003-10-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"SIG13(PRO18)","bibliographicVolumeNumber":"44"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"id":16726,"links":{}}