@CONFERENCE\{IMM1994-01799,
    author       = "M. Fr{\"{a}}nzle and M. Müller-Olm",
    title        = "Towards provably correct code generation for a hard real-time programming language",
    year         = "1994",
    pages        = "294-308",
    booktitle    = "Compiler Construction ({CC}  94)",
    volume       = "786",
    series       = "Lecture Notes in Computer Science",
    editor       = "Peter A. Fritzson",
    publisher    = "Springer Verlag",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/1799-full.html",
    abstract     = "This paper sketches a hard real-time programming language featuring operators for expressing timeliness requirements in an abstract, implementation-independent way and presents parts of the design and verification of a provably correct code generator for that language. The notion of implementation correctness used as an implicit specification of the code generator pays attention to timeliness requirements. Hence, formal verification of the code generator design is a guarantee of meeting all deadlines when executing generated code."
}