Abstract:

Java Byte Code Verification by Model Checking

David Basin and Stefan Friedrich and Joachim Posegga and Harald Vogt


Verification plays a central role in the security of Java bytecode: the Java bytecode verifier performs a 
static analysis to ensure that bytecode loaded over a network has certain security related properties. We 
present an alternative approach to Java bytecode verification based on model-checking.