Java/JVM Exception Handling

Citation: Egon Börger and Wolfram Schulte, "A Practical Method for Specification and Analysis of Exception Handling: A Java/JVM Case Study." IEEE Transactions on Software Engineering, vol. 26, no. 10, October 2000, 872--887.
Summary: ASM models for exception handling in Java and the Java Virtual Machine (JVM) are given, along with a compilation scheme for Java to JVM code. It is proven that corresponding runs of the Java and JVM throw the same exceptions with equivalent effect.
Subjects: Java, Verification
Download: Available from Egon Börger's WWW site in PostScript.
Notes: A different proof has been given in Jbook.