Skip to main content
Book Chapter

Program transformation and compilation

Springer Verlag, (2016), 473-492
DOI: 10.1007/978-3-319-49812-6_14
1Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.
Get full text

Abstract

The main purpose of the KeY system is to ensure program correctness w.r.t. a formal specification on the level of source code. However, a flawed(?) compiler may invalidate correctness properties that have been formally verified for the program’s sourcecode. Hence, we additionally need to guarantee the correctness of the compilation result w.r.t. its source code.

Cite

CITATION STYLE

APA

Ji, R., & Bubel, R. (2016). Program transformation and compilation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10001 LNCS, pp. 473–492). Springer Verlag. https://doi.org/10.1007/978-3-319-49812-6_14

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free