Formalisation and implementation of an algorithm for bytecode verification of @NonNull types
Java's annotation mechanism allows us to extend its type system with non-null types. Checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation. (C) 2010 Elsevier B.V. All rights reserved.
bytecode verification java nonnull types static analysis