Verifying a Compiler for Java Threads

14 years 6 days ago
Verifying a Compiler for Java Threads
Abstract. A verified compiler is an integral part of every security infrastructure. Previous work has come up with formal semantics for sequential and concurrent variants of Java and has proven the correctness of compilers for the sequential part. This paper presents a rigorous formalisation (in the proof assistant Isabelle/HOL) of concurrent Java source and byte code together with an executable compiler and its correctness proof. It guarantees that the generated byte code shows exactly the same observable behaviour as the semantics for the multithreaded source code.
Andreas Lochbihler
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where ESOP
Authors Andreas Lochbihler
Comments (0)