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.
We worked on a type system proposed in \origpaper\ to enforce a
discipline for object initialization in the Java Virtual Machine
Language and implemented it in the Coq \cite{Coq} proof and specification
language. We first produced mechanically checked proofs of the theorems in
\origpaper\ and then we constructed an functional implementation of
a byte-code verifier. We have a mechanical proof that this byte-code
verifier only accepts programs that have a safe behavior with respect
to initialization. Thanks to the extraction mechanism provided in Coq
\cite{PaulinWerner93}, we obtain a program in CAML that can be
directly executed on sample programs.
