Skip to main content

2001 | OriginalPaper | Buchkapitel

Formalizing a JVML Verifier for Initialization in a Theorem Prover

verfasst von : Yves Bertot

Erschienen in: Computer Aided Verification

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

The byte-code verifier is advertised as a key component of the security and safety strategy for the Java language, making it possible to use and exchange Java programs without fearing too much damage due to erroneous programs or malignant program providers. As Java is likely to become one of the languages used to embed programs in all kinds of appliances or computer-based applications, it becomes important to verify that the claim of safety is justified.

Metadaten
Titel
Formalizing a JVML Verifier for Initialization in a Theorem Prover
verfasst von
Yves Bertot
Copyright-Jahr
2001
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/3-540-44585-4_3

Premium Partner