loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
16th IEEE International Conference on Automated Software Engineering (ASE'01)
The Synthesis of a Java Card Tokenization Algorithm
San Diego, California
November 26-November 29
ISBN: 0-7695-1426-X
ASCII Text
x 
 
Ewen Denney, "The Synthesis of a Java Card Tokenization Algorithm," Automated Software Engineering, International Conference on, pp. 43, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001.
 
 
BibTex
x
 
@article{ 10.1109/ASE.2001.989789,
author = {Ewen Denney},
title = {The Synthesis of a Java Card Tokenization Algorithm},
journal ={Automated Software Engineering, International Conference on},
volume = {0},
year = {2001},
isbn = {0-7695-1426-X},
pages = {43},
doi = {http://doi.ieeecomputersociety.org/10.1109/ASE.2001.989789},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Automated Software Engineering, International Conference on
TI - The Synthesis of a Java Card Tokenization Algorithm
SN - 0-7695-1426-X
SP
EP
A1 - Ewen Denney,
PY - 2001
VL - 0
JA - Automated Software Engineering, International Conference on
ER -
 
Ewen Denney, University of Edinburgh
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.
Citation:
Ewen Denney, "The Synthesis of a Java Card Tokenization Algorithm," ase, pp.43, 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.