Lamprecht, Anna-LenaMargaria, TizianaSteffen, BernhardBiel, BettinaBook, MatthiasGruhn, Volker2019-08-132019-08-1320063-88579-173-0https://dl.gi.de/handle/20.500.12116/24305Dieses 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.deText/Conference Paper1617-5468