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

Displayed time zone: Belfast change

14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Nicolas Tabareau Inria
14:00
30m
Research paper
A Verified Protocol Buffer Compiler
CPP
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI
14:30
30m
Research paper
A Coq Mechanised Formal Semantics for Realistic SQL Queries - Formally Reconciling SQL and Bag Relational Algebra
CPP
Véronique Benzaken LRI, Université Paris-Sud, Evelyne Contejean
DOI
15:00
30m
Research paper
Dynamic Class Initialization Semantics: a Jinja Extension
CPP
Susannah Mansky , Elsa Gunter University of Illinois
DOI