This paper presents a case study in verified program compilation from high-level language programs to assembler code using the Cogito formal development system. A form of window-inference based on the Z schema is used to perform the compilation. Data-refinement is used to change the representation of integer variables to assembler word locations.
CITATION STYLE
Wildman, L. (2002). A formal basis for a program compilation proof tool. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2391, pp. 491–510). Springer Verlag. https://doi.org/10.1007/3-540-45614-7_28
Mendeley helps you to discover research relevant for your work.