Pearce, David J; Male, Chris; Dymnikov, Constantine; Potanin, Alex
(Victoria University of Wellington, 2008)
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 ...