Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
435535 | Science of Computer Programming | 2011 | 22 Pages |
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.
Research highlights► We formalise our non-null bytecode verifier for a subset of Java Bytecode. ► We detail an implementation of our system for Java Bytecode. ► We report on our experiences with using our system on real-world programs.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Chris Male, David J. Pearce, Alex Potanin, Constantine Dymnikov,