Art

J-GLOBAL ID：200902207550441700   Reference number：03A0745976

Generation of Program Analyzer Based on Model Checking

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

Author (4)： YAMAOKA YUJI (東大 大学院情報理工学系研究科) ,  HU Z (東大 大学院情報理工学系研究科) ,  TAKEICHI MASATO (東大 大学院情報理工学系研究科) ,  OGAWA MIZUHITO (東大 大学院情報理工学系研究科)
Material： 情報処理学会論文誌  (IPSJ Journal)
Volume： 44  Issue： SIG13(PRO18)  Page： 25-37  Publication year： Oct. 15, 2003 
JST Material Number： Z0778A  ISSN： 0387-5806  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： JAPANESE (JA)

Thesaurus term： *model checking ,...
Semi thesaurus term： software tool ,...

   To see more with JDream III (charged).   {{ this.onShowAbsJLink("http://jdream3.com/lp/jglobal/index.html?docNo=03A0745976&from=J-GLOBAL&jstjournalNo=Z0778A") }}

JST classification (2)： Theory of computation  (JB02000A) ,  Language processors  (JD03040F)

Reference (12)：

• AHO, A. Principles of Compiler Design. 1977
• CLARKE, E. Model Checking. 1999
• CORBETT, J. C. Bandera : extracting finite-state models from Java source code. International Conference on Software Engineering, 2000. 2000, 439-448
• HOLZMANN, G. J. The Model Checker SPIN. Software Engineering. 1997, 23, 5, 279-295
• LACEY, D. Proving correctness of compiler optimizations by temporal logic. Symposium on Principles of Programming Languages, 2002. 2002, 283-294

Terms in the title (3)： モデル検査技術 ,  プログラム解析 ,  ツール