Since PVS is a static source-level checker, I don't see how it would make sense to check JVM bytecode.

Java