| 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. |
Notes:
|
| |
[an error occurred while processing this directive]
URL:
http://web.eecs.umich.edu/gasm/papers/jbytecomplete.html (page only)
last update: Wednesday, 14-Aug-2013 18:19:19 EDT