Journal ArticleOPEN ACCESS

Correctness of java card method lookup via logical relations

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2000) 1782 104-118
DOI: 10.1007/3-540-46425-5_7
5Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

We formalise the Java Card bytecode optimisation from class file to CAP file format as a set of constraints between the two formats, and define and prove its correctness. Java Card bytecode is formalised as an abstract operational semantics, which can then be instantiated into the two formats. The optimisation is given as a logical relation such that the instantiated semantics are observably equal. The proof has been automated using the Coq theorem prover. © Springer-Verlag Berlin Heidelberg 2000.

Cite

CITATION STYLE

APA

Denney, E., & Jensen, T. (2000). Correctness of java card method lookup via logical relations. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1782, 104–118. https://doi.org/10.1007/3-540-46425-5_7

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free