Automated code generation is an enabling technology for model-based software development and promises many benefits, including higher quality and reduced turn-around times. However, the key to realizing these benefits is generator correctness: nothing is gained from replacing manual coding errors with automatic coding errors.

Since the direct verification of generators is unfeasible with existing techniques, "correct-by-construction" approaches have been explored. However, these remain difficult to implement and to scale up, and have not seen widespread use. Currently, generators are validated primarily by testing [8], though this cannot guarantee correctness and quickly becomes excessive. Here we follow an alternative approach based on the observation that the correctness of the generator is irrelevant if instead the correctness of the generated programs is shown individually. Similar to proof carrying code [7], we focus on the Hoare-style certification of specific safety properties. This simplifies our task but still leaves the problem of constructing the appropriate logical annotations (i.e., pre-/postconditions and loop invariants), due to their central role in Hoare-style techniques.