I found an interesting paper on jsr/ret verification. It contains the following example of valid Java code that is not verifiable with the verification algorithm described in the JVM spec:
static int m(boolean x) {
int y;
try {
if(x) return 1;
y = 2;
} finally {
if(x) y = 3;
}
return y;
}