A formal executable semantics of the Java']JavaCard platform

被引：0
|
作者：
Barthe, G [1 ]
Dufay, G
Jakubiec, L
Serpette, B
de Sousa, SM
机构：
[1] INRIA Sophia Antipolis, Sophia Antipolis, France
[2] Univ Aix Marseille 1, Marseille, France
[3] Univ Beira Interior, Covilha, Portugal
来源：
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS | 2001年 / 2028卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present a formal executable specification of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Verifier (BCV). Moreover, we relate both components by giving a proof of correctness of the ByteCode Verifier. Both formalisations and proofs have been machined-checked using the proof assistant Coq.
引用
收藏
页码：302 / 319
页数：18
相关论文
共 50 条
  • [41] Executable semantics for compensating CSP
    Butler, M
    Ripon, S
    FORMAL TECHNIQUES FOR COMPUTER SYSTEMS AND BUSINESS PROCESSES, PROCEEDINGS, 2005, 3670 : 243 - 256
  • [42] Georeferencing with Java']Java: An example of executable metadata
    Rew, RK
    14TH INTERNATIONAL CONFERENCE ON INTERACTIVE INFORMATION AND PROCESSING SYSTEM (IIPS) FOR METEOROLOGY, OCEANOGRAPHY, AND HYDROLOGY, 1998, : 191 - 193
  • [43] Executable structural operational semantics in Maude
    Verdejo, A
    Martí-Oliet, N
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2006, 67 (1-2): : 226 - 293
  • [44] Executable component-based semantics
    van Binsbergen, L. Thomas
    Mosses, Peter D.
    Sculthorpe, Neil
    JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 103 : 184 - 212
  • [45] Executable Semantics of Ethereum Intermediate Language
    Han N.
    Li X.-M.
    Zhang Q.-Y.
    Wang G.-H.
    Shi Z.-P.
    Guan Y.
    Ruan Jian Xue Bao/Journal of Software, 2021, 32 (06): : 1717 - 1732
  • [46] An Executable Semantics of the SystemC UML Profile
    Riccobene, Elvinia
    Scandurra, Patrizia
    ABSTRACT STATE MACHINES, ALLOY, B AND Z, PROCEEDINGS, 2010, 5977 : 75 - +
  • [47] Reification of executable test scripts in formal specification-based test generation: The Java']Java Card Transaction Mechanism case study
    Bouquet, F
    Legeard, B
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 778 - 795
  • [48] What is formal in formal semantics?
    Wolenski, J
    DIALECTICA, 2004, 58 (03) : 427 - 436
  • [49] Model checking of multi-applet Java']JavaCard applications
    Chugunov, G
    Fredlund, LA
    Gurov, D
    USENIX ASSOCIATION AND IFIP WG 8.8 (SMART CARDS) PROCEEDINGS OF CARDIS '02 FIFTH SMART CARD RESEARCH AND ADVANCED APPLICATION CONFERENCE, 2002, : 87 - 95
  • [50] Using Java']JavaCard to guarantee protection for remote mobile agent
    Li Jie
    Wang Ruchuan
    CHINESE JOURNAL OF ELECTRONICS, 2006, 15 (03): : 417 - 421
12345