Java Bytecode Verification

Citation: Robert Stärk and Joachim Schmid, "Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler". Journal of Automated Reasoning 30 (3-4), 2003, 323-361.
Summary: A proof that the Java-to-JVM compiler generates verifiable bytecode. ASMs are used to specify the JVM and the bytecode verifier.
Subjects: Compiler Correctness, Java, Verification
Download: From Robert Stärk's home page in PDF.