Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.

Cornelia Pusch

Browse the full TACAS paper archive.