• Java bytecode verification: al...

Treffer: Java bytecode verification: algorithms and formalizations

Title:
Java bytecode verification: algorithms and formalizations
Authors:
Leroy, Xavier
Contributors:
Typed programming, modularity and compilation (CRISTAL), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Source:
ISSN: 0168-7433.
Publisher Information:
HAL CCSD
Springer Verlag
Publication Year:
2003
Collection:
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe)
Subject Terms:
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Document Type:
Fachzeitschrift article in journal/newspaper
Language:
English
Relation:
hal-01499939; https://hal.inria.fr/hal-01499939; https://hal.inria.fr/hal-01499939/document; https://hal.inria.fr/hal-01499939/file/bytecode-verification-JAR.pdf
DOI:
10.1023/A:1025055424017
Availability:
https://hal.inria.fr/hal-01499939
https://hal.inria.fr/hal-01499939/document
https://hal.inria.fr/hal-01499939/file/bytecode-verification-JAR.pdf
https://doi.org/10.1023/A:1025055424017
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edsbas.1CFEFB63
Database:
BASE

Weitere Informationen

International audience ; Bytecode verification is a crucial security component for Java applets, on the Web and on embedded devices such as smart cards. This paper reviews the various bytecode verification algorithms that have been proposed, recasts them in a common framework of dataflow analysis, and surveys the use of proof assistants to specify bytecode verification and prove its correctness.