Sophia Drossopoulou (Imperial College, Univ. of London)
Title: Towards a model of dynamic linking and verification for Java
Abstract. We develop a model for dynamic linking and verification as in Java. We distinguish four components in a JVM (Java virtual machine), ie evaluation, loading, verification and resolution, with their associated checks. We demonstrate how these four together guarantee type soundness. We take an abstract view, and base our model on a language nearer to Java source than the byte-code. We concentrate on giving a comprehensive description of the role the JVM components and their dependencies, rather than a faithful model of each in separation. Thus the model is independent of the particulars of the byte code language.