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 条
  • [31] The KRAKATOA tool for certification of JAVA']JAVA/JAVA']JAVACARD programs annotated in JML
    Marché, C
    Paulin-Mohring, C
    Urbain, X
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2004, 58 (1-2): : 89 - 106
  • [32] An Executable and Testable Semantics for iTasks
    Koopman, Pieter
    Plasmeijer, Rinus
    Achten, Peter
    [J]. IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES, 2011, 5836 : 212 - 232
  • [33] Qualified Electronic Signature via SIM Card Using Java']JavaCard 3 Connected Edition Platform
    Breier, Jakub
    Pomothy, Adam
    [J]. 2014 NINTH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY (ARES), 2015, : 349 - 355
  • [34] ExAIS: Executable AI Semantics
    Schutni, Richard
    Sun, Jun
    [J]. 2022 ACM/IEEE 44TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2022), 2022, : 859 - 870
  • [35] EXECUTABLE SPECIFICATION OF STATIC SEMANTICS
    DESPEYROUX, T
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1984, 173 : 215 - 233
  • [36] Executable semantics for compensating CSP
    Butler, M
    Ripon, S
    [J]. FORMAL TECHNIQUES FOR COMPUTER SYSTEMS AND BUSINESS PROCESSES, PROCEEDINGS, 2005, 3670 : 243 - 256
  • [37] Georeferencing with Java']Java: An example of executable metadata
    Rew, RK
    [J]. 14TH INTERNATIONAL CONFERENCE ON INTERACTIVE INFORMATION AND PROCESSING SYSTEM (IIPS) FOR METEOROLOGY, OCEANOGRAPHY, AND HYDROLOGY, 1998, : 191 - 193
  • [38] Executable structural operational semantics in Maude
    Verdejo, A
    Martí-Oliet, N
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2006, 67 (1-2): : 226 - 293
  • [39] Executable component-based semantics
    van Binsbergen, L. Thomas
    Mosses, Peter D.
    Sculthorpe, Neil
    [J]. JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2019, 103 : 184 - 212
  • [40] Executable Semantics of Ethereum Intermediate Language
    Han, Ning
    Li, Xi-Meng
    Zhang, Qian-Ying
    Wang, Guo-Hui
    Shi, Zhi-Ping
    Guan, Yong
    [J]. Ruan Jian Xue Bao/Journal of Software, 2021, 32 (06): : 1717 - 1732
12345