- 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.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0143,
- author = {
Ewen Denney
},
- title = {The Synthesis of a Java Card Tokenisation Algorithm},
- book title = {Proceedings of the 16th IEEE International Conference on Automated Software Engineering},
- year = 2001,
- month = {Nov},
- }
|
