The synthesis of a Java']Java Card tokenisation algorithm

被引：2
|
作者：
Denney, E [1 ]
机构：
[1] Univ Edinburgh, Div Informat, Edinburgh, Midlothian, Scotland
来源：
16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS | 2001年
关键词：
D O I：
10.1109/ASE.2001.989789
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We describe the development of a Java bytecode optimisation algorithm by the methodology of program extraction. We develop the algorithm as a collection of proofs and definitions in the Coq proof assistant, and then use Coq's extraction mechanism to automatically generate a program in OCaml. The extraction methodology guarantees that this program is correct. We discuss the feasibility of the methodology and suggest some improvements that could be made.
引用
收藏
页码：43 / 50
页数：8
相关论文
共 50 条
  • [1] Tokenisation and compression of Java']Java class files
    Haggett, Shawn
    Knowles, Greg
    [J]. JOURNAL OF SYSTEMS ARCHITECTURE, 2012, 58 (01) : 1 - 12
  • [2] Tokenisation of class files for an embedded Java']Java processor
    Haggett, Shawn
    Knowles, Greg
    Bignell, Graham
    [J]. 6TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, PROCEEDINGS, 2007, : 375 - +
  • [3] An asymmetric fingerprint matching algorithm for Java']Java Card™
    Bistarelli, Stefano
    Santini, Francesco
    Vaccarelli, Anna
    [J]. PATTERN ANALYSIS AND APPLICATIONS, 2006, 9 (04) : 359 - 376
  • [4] An asymmetric fingerprint matching algorithm for Java']Java Card™
    Bistarelli, S
    Santini, F
    Vaccarelli, A
    [J]. AUDIO AND VIDEO BASED BIOMETRIC PERSON AUTHENTICATION, PROCEEDINGS, 2005, 3546 : 279 - 288
  • [5] Comparison Analysis of Acorn Algorithm and Snow Algorithm on Smart Card using Java']Java Card
    Nurwarsito, Heru
    Ayu, Sarah Kusuma
    [J]. 2021 4TH INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATICS ENGINEERING (IC2IE 2021), 2021, : 429 - 434
  • [6] Reverse engineering a Java']Java Card memory management algorithm
    Mesbah, Abdelhak
    Lanet, Jean-Louis
    Mezghiche, Mohamed
    [J]. COMPUTERS & SECURITY, 2017, 66 : 97 - 114
  • [7] Improved Adaptive Generational Garbage Collection Algorithm for Java']Java Card
    Yang Fubiao
    Li Daiping
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON LOGISTICS, ENGINEERING, MANAGEMENT AND COMPUTER SCIENCE, 2014, 101 : 699 - 702
  • [8] Biometric Hash Algorithm for Dynamic Handwriting Embedded on a Java']Java Card
    Kuemmel, Karl
    Vielhauer, Claus
    [J]. BIOMETRICS AND ID MANAGEMENT, 2011, 6583 : 61 - 72
  • [9] Using contour marking bytecode verification algorithm on the java']java card
    Jiang, Longlong
    Li, Daiping
    [J]. MECHATRONICS ENGINEERING, COMPUTING AND INFORMATION TECHNOLOGY, 2014, 556-562 : 4120 - +
  • [10] 8-bit Java']Java: the Java']Java card
    Grehan, R
    [J]. COMPUTER DESIGN, 1997, 36 (05): : 80 - 80
12345