[lochbihler10esop] | Andreas Lochbihler, Verifying a Compiler for Java Threads, A. D. Gordon (Ed.), European Symposium on Programming (ESOP'10), pp. 427--447, Springer, March 2010.
|
Zusammenfassung
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.
Download
Original article available at springerlink.com.
BibTeX
Institutsinterne Autoren
Projekte