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] An Executable Formal Semantics of PHP
    Filaretti, Daniele
    Maffeis, Sergio
    [J]. ECOOP 2014 - OBJECT-ORIENTED PROGRAMMING, 2014, 8586 : 567 - 592
  • [2] KRust: A Formal Executable Semantics of Rust
    Wang, Feng
    Song, Fu
    Zhang, Min
    Zhu, Xiaoran
    Zhang, Jun
    [J]. PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018), 2018, : 44 - 51
  • [3] An Executable Formal Semantics of C with Applications
    Ellison, Chucky
    Rosu, Grigore
    [J]. ACM SIGPLAN NOTICES, 2012, 47 (01) : 533 - 544
  • [4] An Executable Formal Semantics of C with Applications
    Ellison, Chucky
    Rosu, Grigore
    [J]. POPL 12: PROCEEDINGS OF THE 39TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2012, : 533 - 544
  • [5] Executable Formal Semantics for the POSIX Shell
    Greenberg, Michael
    Blatt, Austin J.
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
  • [6] Formal specification of the Java']JavaCard API in JML: the APDU class
    Poll, E
    van den Berg, J
    Jacobs, B
    [J]. COMPUTER NETWORKS, 2001, 36 (04) : 407 - 421
  • [7] A Formal Framework for Prototyping Executable Semantics in ATL
    Boronat, Artur
    [J]. THEORY AND PRACTICE OF MODEL TRANSFORMATION, ICMT 2018, 2018, 10888 : 157 - 172
  • [8] An executable formal semantics for UML-RT
    Posse, Ernesto
    Dingel, Juergen
    [J]. SOFTWARE AND SYSTEMS MODELING, 2016, 15 (01): : 179 - 217
  • [9] Formal executable semantics for conformance in the MDE framework
    Egea, Marina
    Rusu, Vlad
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (1-2) : 73 - 81
  • [10] An executable formal semantics for UML-RT
    Ernesto Posse
    Juergen Dingel
    [J]. Software & Systems Modeling, 2016, 15 : 179 - 217
12345