Programme, die verst?rkt auf dynamischen Speicher und Pointer zurückgreifen, sind bekanntlich besonders schwer zu analysieren, insbesondere wenn Programmierer die von Programmiersprachen wie C erm?glichten Freiheiten aussch?pfen. Dieses Forschungsprojekt zielt darauf ab, Programmanalysen dadurch zu vereinfachen, dass die in einem Programm verwendeten dynamischen Datenstrukturen zun?chst identifiziert werden. Die von uns angestrebte automatische Identifikation schlie?t dabei nicht nur die Datenstruktur (z. B. eine einfach verkettete Liste) sondern auch deren Verhalten ein (z. B. eine einfach verkettete Liste verwendet als Queue oder Stack).

Zur Identifikation einer Datenstruktur und deren Verhalten ist es zun?chst notwendig, diejenigen Operationen zu analysieren, welche die Datenstruktur von einem Speicherzustand zum darauf folgenden transformieren. Dazu verwenden wir eine dynamische Analyse, bei der das zu untersuchende Programm so instrumentiert wird, dass die von ihm verursachte Sequenz von Speicherzust?nden zur Programmlaufzeit zurückgewonnen werden kann. Mit Hilfe von Techniken des maschinellen Lernens suchen wir in dieser Sequenz zuerst nach sich wiederholenden Mustern, die durch ein mehrfaches Ausführen von Code-Fragmenten verursacht werden. Falls dabei Operationen auf dynamischen Datenstrukturen ausgeführt werden (z. B. Einfügen am Ende oder L?schen in einer einfach verketteten Liste), so pr?sentieren einige dieser Muster die zu den Operationen geh?renden Code-Fragmente. Um die Operationen zu benennen, benutzen wir Techniken des Pattern Matching, welche die durch die identifizierten Code-Fragmente verursachten Speichertransformationen analysieren. Die verwendete Kombination von Operationen, die eine bestimmte Datenstruktur manipulieren, erlaubt uns schlie?lich, das Verhalten der Datenstruktur zu bestimmen.

?ber den offensichtlichen Nutzen eines verbesserten Programmverst?ndnisses hinaus, wenden wir unsere Technik auch im Bereich der formalen Programmverifikation an. Dazu kollaborieren wir mit Verifikationsexperten der University of York, Gro?britannien im Rahmen des Forschungsprojekts Moderne Heap-Analyse und -Verifikation, welches durch die Deutsche Forschungsgemeinschaft (DFG) gef?rdert wird (Projekt-Nr. LU 1748/2-1), sowie mit Dr. Jan Tobias Mühlberg (K.U. Leuven, Belgien).

球探足球比分: Dr. David White

Publikationen:

• White, D. H. and Lüttgen, G. Identifying dynamic data structures by learning evolving patterns in memory. In N. Piterman and S. A. Smolka, eds., 19th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), vol. 7795 of Lecture Notes in Computer Science, pp. 354-369, Rome, Italy, March 2013. Springer-Verlag.