Pearce, David JMale, ChrisDymnikov, ConstantinePotanin, Alex2008-07-242022-07-062008-07-242022-07-0620082008https://ir.wgtn.ac.nz/handle/123456789/18842Java'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.pdfen-NZThe original publication is available at www.springerlink.comNon-null type verificationJava programmingNullPointerExceptionsTextSpringer