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
• Antragstellende Institution: Technische Universität München (TUM)
• Mitantragstellende Institution: Ludwig-Maximilians-Universität München
• Sprecher: Professor Dr. Helmut Seidl
• beteiligte Wissenschaftlerinnen / beteiligte Wissenschaftler: Professor Dr. Javier Esparza; Professor Dr. Martin Hofmann (†); Professor Dr.-Ing. Alois Knoll; Professor Tobias Nipkow, Ph.D.; Professor Dr. Andrey Rybalchenko; Professorin Dr.-Ing. Birgit Vogel-Heuser