Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 15:00 - 15:30 at Sala XII - Research Papers: Program Verification Chair(s): Nicolas Tabareau

The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a \texttt{new} or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.

Tue 15 Jan

14:00 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Nicolas TabareauInria
CPP-201914:00 - 14:30
Research paper
Qianchuan YePurdue University, Benjamin DelawarePurdue University
CPP-201914:30 - 15:00
Research paper
Véronique BenzakenLRI, Université Paris-Sud, Evelyne Contejean
CPP-201915:00 - 15:30
Research paper
Susannah Mansky, Elsa GunterUniversity of Illinois