Java bytecode verification: an overview

Xavier Leroy (1)

1 CRISTAL - Typed programming, modularity and compilation

Bytecode verification is a crucial security component for Java applets, on the Web and on embedded devices such as smart cards. This paper describes the main bytecode verification algorithms and surveys the variety of formal methods that have been applied to bytecode verification in order to establish its correctness.

Domaines: Langage de programmation [cs.PL]

Xavier Leroy. Java bytecode verification: an overview. Computer Aided Verification, CAV 2001, Jul 2001, Paris, France. pp.265-285, ⟨10.1007/3-540-44585-4_26⟩. ⟨hal-01499955⟩