A programming logic for Java']Java bytecode programs

被引：0
|
作者：
Quigley, CL [1 ]
机构：
[1] Univ Glasgow, Dept Comp Sci, Glasgow G12 8QQ, Lanark, Scotland
来源：
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2003年 / 2758卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Using the Isabelle theorem prover [10] we have developed a programming logic for Java bytecode, and demonstrated that it can be used to prove properties of simple bytecode programs involving loops. Our motivation for this was to produce a method by which Java Just-In-Time (JIT) compilers could be assisted to produce more efficient code. This paper discusses the issues involved in the development of the programming logic as it stands, and suggests possible extensions to it. We also describe our experiences of the difficulties inherent in carrying out proof at the level of bytecode instructions, along with the benefits and disadvantages of using a mechanized proof tool.
引用
收藏
页码：41 / 54
页数：14
相关论文
共 50 条
  • [1] Verification of Java']Java bytecode using analysis and transformation of logic programs
    Albert, E.
    Gomez-Zamalloa, M.
    Hubert, L.
    Puebla, G.
    [J]. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2007, 4354 : 124 - +
  • [2] Path Executions of Java']Java Bytecode Programs
    Soomro, Safeeullah
    Alansari, Zainab
    Belgaum, Mohammad Riyaz
    [J]. PROGRESS IN ADVANCED COMPUTING AND INTELLIGENT ENGINEERING, VOL 2, 2018, 564 : 261 - 271
  • [3] A Framework for Debugging Java']Java Programs in a Bytecode
    Soomro, Safeeullah
    Belgaum, Mohammad Riyaz
    Alansari, Zainab
    Miraz, Mahdi H.
    [J]. 2018 INTERNATIONAL CONFERENCE ON COMPUTING, ELECTRONICS & COMMUNICATIONS ENGINEERING (ICCECE), 2018, : 317 - 322
  • [4] Dynamic slicing of Java']Java bytecode programs
    Szegedi, A
    Gyimóthy, T
    [J]. FIFTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2005, : 35 - 44
  • [5] An empirical study of Java']Java bytecode programs
    Collberg, Christian
    Myles, Ginger
    Stepp, Michael
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 2007, 37 (06): : 581 - 641
  • [6] Compiling C++ programs to Java']Java bytecode
    Hu, GZ
    Gadapa, A
    [J]. SIXTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERNG, ARTIFICIAL INTELLIGENCE, NETWORKING AND PARALLEL/DISTRIBUTED COMPUTING AND FIRST AICS INTERNATIONAL WORKSHOP ON SELF-ASSEMBLING WIRELESS NETWORKS, PROCEEDINGS, 2005, : 56 - 61
  • [7] Compiling lazy functional programs to Java']Java bytecode
    Meehan, G
    Joy, M
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 1999, 29 (07): : 617 - 645
  • [8] Constraint based Testing and Verification of Java']Java Bytecode Programs
    Achour, Safaa
    Benattou, Mohammed
    [J]. 2018 IEEE 5TH INTERNATIONAL CONGRESS ON INFORMATION SCIENCE AND TECHNOLOGY (IEEE CIST'18), 2018, : 64 - 69
  • [9] A Heap Model for Java']Java Bytecode to Support Separation Logic
    Luo, Chenguang
    He, Guanhua
    Qin, Shengchao
    [J]. APSEC 2008:15TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2008, : 127 - 134
  • [10] Distributed Java']Java Bytecode Genetic Programming with telecom applications
    Lukschandl, E
    Borgvall, H
    Nohle, L
    Nordahl, M
    Nordin, P
    [J]. GENETIC PROGRAMMING, PROCEEDINGS, 2000, 1802 : 316 - 325
12345