DocumentCode
2338974
Title
The synthesis of a Java card tokenisation algorithm
Author
Denney, Ewen
Author_Institution
Div. of Informatics, Edinburgh Univ., UK
fYear
2001
fDate
26-29 Nov. 2001
Firstpage
43
Lastpage
50
Abstract
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.
Keywords
Java; automatic programming; optimising compilers; theorem proving; Coq proof assistant; Java byte code optimisation algorithm; Java card tokenisation algorithm synthesis; OCaml; extraction mechanism; extraction methodology; program correctness; program extraction; proofs; Automation; Calculus; Computer bugs; Computer industry; Constraint optimization; Formal verification; Functional programming; Informatics; Java; Smart cards;
fLanguage
English
Publisher
ieee
Conference_Titel
Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on
ISSN
1938-4300
Print_ISBN
0-7695-1426-X
Type
conf
DOI
10.1109/ASE.2001.989789
Filename
989789
Link To Document