Abstract
Safety-Critical Java (SCJ) is a version of Java that facilitates the development of certifiable programs, and requires a specialised virtual machine (SCJVM). In spite of the nature of the applications for which SCJ is designed, none of the SCJVMs are verified. In this paper, we contribute a formal specification of a bytecode interpreter for SCJ and an algebraic compilation strategy from Java bytecode to C. For the target C code, we adopt the compilation approach for icecap, the only SCJVM that is open source and up-to-date with the SCJ standard. Our work enables either prototyping of a verified compiler, or full verification of icecap or any other SCJVM.
Cite
CITATION STYLE
Baxter, J., & Cavalcanti, A. (2017). Algebraic compilation of safety-critical Java bytecode. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10510 LNCS, pp. 161–176). Springer Verlag. https://doi.org/10.1007/978-3-319-66845-1_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
