Optimal Interprocedural Analysis of Programs with Thread Creation (1st funding period) (OpIAT)

Basic data for this project

Type of project: Individual project
Duration: 20/09/2007 - 30/11/2012 | 1st Funding period

Description

Die Bedeutung von Nebenläufigkeit hat in den vergangenen Jahren beständig zugenommen.Zum einen wird Nebenläufigkeit in Form von Multi-Threading bei der Programmierung routinemäßig etwa zur Konstruktion graphischer Benutzeroberflächen und anderer reaktiver Systeme benutzt. Zum zweiten führt die Vernetzung von Rechnern z.B. durch das Internet zu Nebenläufigkeittsphänomenen. Außerdem werden zunehmend Parallelprozessoren eingesetzt, da andere Mittel der Leistungssteigerung an physikalische Grenzen stoßen. Nebenläufige Programme sind wegen der zeitlich nicht genau festgelegten Verzahnung der Aktivitäten inhärent nicht-deterministisch und damit schlecht testbar. Daher sind statische Analyseverfahren für Verifikations- und Validierungszwecke unerlässlich. Ziel dieses Projektes ist es deshalb, Methoden zur automatischen Analyse von Programmen mit rekursiven Prozeduren und dynamischer Erzeugung von Threads zu entwickeln, die existierenden Verfahren im Hinblick auf Effizienz, Präzision oder Ausdruckskraft überlegen sind. Dabei interessieren wir uns besonders für Verfahren, die Informationen nur auf kontrollierte Weise aufgeben und für die deshalb Garantien für die erzielte Präzision gegeben werden können, sogenannte optimale Analysen. Das Projekt wird in Kooperation mit der Gruppe von Prof. Helmut Seidl von der TU München durchgeführt und wird durch die DFG (Deutsche Forschungsgemeinschaft) gefördert.

Keywords: Abstract interpretation; concurrency; data flow analysis; program verification; software reliability; static analysis