Dr. David J. Pearce

Formalisation and Implementation of an Algorithm for Bytecode Verification of @NonNull Types

Author(s). Chris Male, David J. Pearce, Alex Potanin and Constantine Dymnikov.

Venue. In Science of Computer Programming, 76 (7), pages 587--608, 2011. ©Elsevier

Abstract. 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.

Related Project(s)