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 条
  • [1] A formal executable semantics of the javacard platform
    Barthe, Gilles
    Dufay, Guillaume
    Jakubiec, Line
    Serpette, Bernard
    de Sousa, Simâo Melo
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2001, 2028 : 302 - 319
  • [2] An Executable Formal Semantics of PHP
    Filaretti, Daniele
    Maffeis, Sergio
    ECOOP 2014 - OBJECT-ORIENTED PROGRAMMING, 2014, 8586 : 567 - 592
  • [3] KRust: A Formal Executable Semantics of Rust
    Wang, Feng
    Song, Fu
    Zhang, Min
    Zhu, Xiaoran
    Zhang, Jun
    PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018), 2018, : 44 - 51
  • [4] An Executable Formal Semantics of C with Applications
    Ellison, Chucky
    Rosu, Grigore
    ACM SIGPLAN NOTICES, 2012, 47 (01) : 533 - 544
  • [5] Executable Formal Semantics for the POSIX Shell
    Greenberg, Michael
    Blatt, Austin J.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [6] An Executable Formal Semantics of C with Applications
    Ellison, Chucky
    Rosu, Grigore
    POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 533 - 544
  • [7] Formal specification of the Java']JavaCard API in JML: the APDU class
    Poll, E
    van den Berg, J
    Jacobs, B
    COMPUTER NETWORKS, 2001, 36 (04) : 407 - 421
  • [8] A Formal Framework for Prototyping Executable Semantics in ATL
    Boronat, Artur
    THEORY AND PRACTICE OF MODEL TRANSFORMATION, ICMT 2018, 2018, 10888 : 157 - 172
  • [9] An executable formal semantics for UML-RT
    Posse, Ernesto
    Dingel, Juergen
    SOFTWARE AND SYSTEMS MODELING, 2016, 15 (01): : 179 - 217
  • [10] Synthesizing Formal Semantics from Executable Interpreters
    Liu, Jiangyi
    Murphy, Charlie
    Grover, Anvay
    Johnson, Keith J. C.
    Reps, Thomas
    D'Antoni, Loris
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (OOPSLA):
12345