Balogh András: Correctness-proven code generation for MDA : [abstract].