Please use this identifier to cite or link to this item:
https://hdl.handle.net/20.500.12008/3498
How to cite
| Title: | An approach to subroutine elimination |
| Authors: | Rodríguez Viacava, Leonardo |
| Type: | Reporte técnico |
| Keywords: | BYTE CODE VERIFIERS, SUBROUTINES, JAVA CARD, CQQ, FORMAL PROOFS |
| Issue Date: | 2003 |
| Abstract: | Subroutines seem to be more a problem than a solution for the Byte Code Verifier's world, especially with resource constrained devices like Java Card. The elimination of subroutines form the Java bytecode would allow the construction of more efficient and precise Byte Code Verifiers. Here we specify a transformation for eliminating subroutines and we prove that its preserves the semantics of the Java program been transformed. Al this is done on top of the COQ Proof Assistant. |
| Publisher: | UR. FI – INCO. |
| Series or collection: | Reportes Técnicos 03-13 |
| ISSN: | 0797-6410 |
| Citation: | RODRÍGUEZ VIACAVA, L. "An approach to subroutine elimination". Reportes Técnicos 03-13. UR. FI – INCO, 2003. |
| License: | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| Appears in Collections: | Reportes Técnicos - Instituto de Computación |
Files in This Item:
| File | Description | Size | Format | ||
|---|---|---|---|---|---|
| TR0313.pdf | 127,63 kB | Adobe PDF | View/Open |
This item is licensed under a Creative Commons License
