An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier