Verifying a compiler for Java threads

FREE-DOWNLOADA Lochbihler – Programming Languages and Systems, 2010
Abstract. A verified compiler is an integral part of every security infra- structure. Previous work
has come up with formal semantics for sequen- tial and concurrent variants of Java and has proven
the correctness of compilers for the sequential part. This paper presents a rigorous