Paper Info
Title
Towards Demonstrably Correct Compilation of Java Byte Code
Abstract
In this paper we investigate the feasibility of a demonstrably correct compiler for Java bytecode. We first examine the suitability of adapting the existing high assurance compiler DeCCo for the Pascal-like language PASP, based on a Z formalisation of the compiler manually transcribed to Prolog. During the investigation we have uncovered several problematic issues and argue that these can be avoided by formally deriving the code of the compiler from the formal specification, rather than manually transcribing it. We have conducted a case study, developing a compiler for a subset of Java bytecode to an idealised RISC processor using the B-method. We show that refinement is a natural way to model compilation and that the B-method can in principle be used to develop a demonstrably correct compiler. In particular, the tool support for B turned out to be extremely valuable: animation, automated refinement checking, and proof each uncovered a series of mistakes.
Year
DOI
Venue
2008
10.1007/978-3-642-04167-9_7
FMCO
Keywords
Field
DocType
idealised risc processor,existing high assurance compiler,towards demonstrably correct compilation,formal specification,demonstrably correct compiler,java bytecode,case study,z formalisation,pascal-like language,automated refinement checking,java byte code,model compilation,b method
Functional compiler,Dynamic compilation,Programming language,Computer science,Compiler correctness,Real-time computing,Compiler,Bootstrapping (compilers),Java bytecode,Compiler construction,Java Modeling Language
Conference
Volume
ISSN
Citations 
5751
0302-9743
1
PageRank 
References 
Authors
0.36
23
1
Name
Order
Citations
PageRank
Michael Leuschel12156135.89