G. Barthe and G. Dufay.
A Tool-Assisted Framework for Certified Bytecode Verification.
In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings
of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages
99-113, Barcelona, Spain, March 2004. Springer-Verlag.
[ bib |
.ps.gz ]
G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa.
A formal correspondence between offensive and defensive JavaCard
virtual machines.
In A. Cortesi, editor, Proceedings of VMCAI'02, volume 2294 of
Lecture Notes in Computer Science, pages 32-45. Springer-Verlag, 2002.
[ bib |
.ps.gz ]
G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa.
A Formal Executable Semantics of the JavaCard Platform.
In D. Sands, editor, Proceedings of ESOP'01, volume 2028 of
Lecture Notes in Computer Science, pages 302-319. Springer-Verlag,
2001.
[ bib |
.ps.gz ]