Correctness of Java']Java Card method lookup via logical relations

被引：0
|
作者：
Denney, E
Jensen, T
机构：
[1] CNRS, IRISA, F-35042 Rennes, France
[2] Univ Edinburgh, Math Reasoning Grp, Div Informat, Edinburgh EH1 1HN, Midlothian, Scotland
来源：
THEORETICAL COMPUTER SCIENCE | 2002年 / 283卷 / 02期
关键词：
compiler correctness; optimisation; operational semantics; !text type='Java']Java[!/text; smart cards;
D O I：
10.1016/S0304-3975(01)00138-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This article presents a formalisation of the bytecode optimisation of Sun's Java Card language from the class file to CAP file format as a set of constraints between the two formats, and defines and proves its correctness. Java Card bytecode is formalised using an abstract operational semantics, which can then be instantiated into the two formats. The optimisation is given as a logical relation such that the instantiated semantics are observably equal. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
下载
收藏
页码：305 / 331
页数：27
相关论文
共 50 条
  • [41] Advanced control flow in Java']Java card programming
    Li, P
    Zdancewic, S
    ACM SIGPLAN NOTICES, 2004, 39 (07) : 165 - 174
  • [42] Verification of JAVA']JAVA CARD applets behavior with respect to transactions and card tears
    Marche, Claude
    Rousset, Nicolas
    SEFM 2006: FOURTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2006, : 137 - +
  • [43] Specification and Runtime Verification of Java']Java Card Programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placido A.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 61 - 78
  • [44] Secure object flow analysis for Java']Java Card
    Éluard, M
    Jensen, T
    USENIX ASSOCIATION AND IFIP WG 8.8 (SMART CARDS) PROCEEDINGS OF CARDIS '02 FIFTH SMART CARD RESEARCH AND ADVANCED APPLICATION CONFERENCE, 2002, : 97 - 110
  • [45] A secure object sharing scheme for Java']Java Card
    Zhang, JQ
    Varadharajan, V
    Mu, Y
    INFORMATION AND COMMUNICATIONS SECURITY, PROCEEDINGS, 2002, 2513 : 243 - 251
  • [46] Developing JAVA']JAVA Card Application with RMI API
    Xu JunWu
    Liang JunLing
    INTERNATIONAL CONFERENCE ON SOLID STATE DEVICES AND MATERIALS SCIENCE, 2012, 25 : 643 - 650
  • [47] Static program analysis for Java']Java Card applets
    Almaliotis, Vasilios
    Loizidis, Alexandros
    Katsaros, Panagiotis
    Louridas, Panagiotis
    Spinellis, Diomidis
    SMART CARD RESEARCH AND ADVANCED APPLICATIONS, PROCEEDINGS, 2008, 5189 : 17 - +
  • [48] A Java']Java processor suitable for applications of Smart Card
    Zhang, JJ
    Li, FH
    Ge, YQ
    Yue, ZW
    Yang, ZL
    2001 4TH INTERNATIONAL CONFERENCE ON ASIC PROCEEDINGS, 2001, : 736 - 739
  • [49] An asymmetric fingerprint matching algorithm for Java']Java Card™
    Bistarelli, Stefano
    Santini, Francesco
    Vaccarelli, Anna
    PATTERN ANALYSIS AND APPLICATIONS, 2006, 9 (04) : 359 - 376
  • [50] High Performance Java']Java Card Operating System
    Eletriby, Mohammad R.
    Sobh, Mohamed
    Bahaa-Eldin, Ayman M.
    Fahmy, Hossam M. A.
    2014 EIGHTH INTERNATIONAL CONFERENCE ON SOFTWARE SECURITY AND RELIABILITY, 2014, : 30 - 39
12345