Data Flow Analysis as a General Concept for the Transport of Verifiable Program Annotations. - Wolfram Amme; Marc-André Möller; Philipp Adler (COCV@ETAPS, 2006)