Dieses Papier beschreibt wie das jABC (eine generische Umgebung für bibliotheksbasierte Programmentwicklung) zusammen mit zwei seiner Plugins (der Modelchecker und ein Flussgraph-Konverter) ein Framework, DFA-MC, für intraprozedurale Datenflussanalyse als Modelchecking bildet. Basierend auf Funktionalitäten, die von der Programmanalyseplattform Soot bereitgestellt werden, generiert der Konverter Graphstrukturen aus Java-Klassen. Die Datenflussanalysen werden dann als Formeln im modalen $μ$-Kalkül ausgedrückt. Die Analyse selbst wird ausgeführt, indem der Modelchecker die Gültigkeit der Formel auf dem Flussgraphen überprüft.