Java Bytecode Verification for @NonNull Types

Java's annotation mechanism allows us to extend its type system with non-null types. However, 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.

• Type: Conference
• Year: 2008
• Where: CC
• Authors: Chris Male, David J. Pearce, Alex Potanin, Constantine Dymnikov
• Keywords: Bytecode Verification Algorithm, CC 2008, Java's Annotation Mechanism, Non-null Types, System Software