GRK 1480:
PUMA Programm- und Modell-Analyse
Fachliche Zuordnung
Informatik
Förderung
Förderung von 2008 bis 2017
Projektkennung
Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 47140942
Wesentliche Aufgabe der Programm- und Modell-Analyse ist das Aufdecken von Programmierfehlern bzw. der Nachweis, dass ein gegebenes Programm korrekt ist, das heißt, sich gemäß seiner Spezifikation verhält. Eine solche Spezifikation kann dabei ganz einfach nur verlangen, dass bestimmte Fehler (wie etwa die Dereferenzierung eines Null-Pointers) nicht vorkommen, oder aber genaue Vorgaben über den Ressourcenverbrauch oder das Ein-/Ausgabe-Verhalten machen. Gerade im Umfeld softwareintensiver Systeme spielen garantierte Eigenschaften eine wichtige Rolle: Das Überwachungssystem eines Intensivpatienten muss zügig auf Änderungen der Messwerte reagieren. Bei einer elektronischen Überweisung muss das Geld nicht nur von dem Konto des Auftraggebers abgebucht, sondern dem Konto des Empfängers gutgeschrieben werden. Ein Verstoß gegen diese Anforderungen hätte im besten Fall große finanzielle Einbußen, im schlimmsten Fall Schaden für Leib und Leben von Personen zur Folge. Es gibt derzeit vier konkurrierende Ansätze zur Modell- und Programm-Analyse: Verifikation durch Theorembeweise, Model Checking, Abstrakte Interpretation und Typsysteme. Jeder dieser Ansätze wird in einer bedeutenden internationalen Community weiter entwickelt und kann auf eine lange Erfolgsgeschichte verweisen. Alle vier Ansätze sind an den Münchner Universitäten stark vertreten. Gerade die Wechselwirkung zwischen unterschiedlichen Ansätzen hat zu neuen praktischen Verfahren geführt. Die Untersuchung solcher Wechselwirkungen, die Entwicklung neuer Methoden im Spannungsfeld der existierenden Vorgehensweisen und ihre Umsetzung in praktisch nutzbare Tools ist das Ziel des Graduiertenkollegs PUMA. Unsere Vision ist der "Verifying Compiler", das heißt die Entwicklung von Methoden und Werkzeugen, mit denen es möglich ist, für ein Stück Software oder ein Software-Modell mit der gleichen Leichtigkeit Eigenschaften zu garantieren wie mit einem Compiler Code zu erzeugen.
DFG-Verfahren
Graduiertenkollegs
