Optimale Interprozedurale Analyse von Programmen mit dynamischer Thread-Erzeugung (OpIAT)

Grunddaten zu diesem Projekt

Art des ProjektesGefördertes Einzelprojekt
Laufzeit an der Universität Münster01.12.2012 - 31.12.2015 | 2. Förderperiode

Beschreibung

Dieses Projekt setzt das OPIAT-Projekt fort. In der ersten Projektphase wurden Methoden entwickelt, um den Kontrollfuss in nebenläufigen Programmen mit Synchronisationsprimitiven präzise zu analysieren. Dabei konzentrierten wir uns einerseits auf dynamische Pushdown-Netzwerke (DPNs) mit wohlgeschachtelten Locks oder Monitoren. Auf der anderen Seite untersuchten wir ein vereinfachtes Taskmodell, das dem Automobilstandard OSWK zu Grunde liegt, bei dem unterschiedliche Tasks mit Hilfe von Ressourcen und Prioritäten synchronisiert werden. Darauf aufbauend sollen nun in dem Nachfolgeprojekt für diese Programmiermodelle Analyseframeworks entwickelt werden, die es erlauben, weiterreichende Programmeigenschaften statisch zu ermitteln. Insbesondere sollen sowohl für das OSEK-Modell als auch für DPNs Wertanalysen für Programme mit globalen Variablen entwickelt werden. Zur Steigerung der Päzision sollen diese Analysen Synchronisationsprimitive mitberüksichtigen. Neben den schon in der ersten Projektphase betrachteten Synchronisationsprimitiven sollen zudem weitere Synchronisationskonzepte identi ziert werden, die exakt behandelt werden können. 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.

StichwörterAbstrakte Interpretation; Datenflussanalyse; Nebenläufigkeit; Programmverifikation; Softwarezuverlässigkeit; statische Analyse
FörderkennzeichenMU 1508/1-2
Mittelgeber / Förderformat
  • DFG - Sachbeihilfe/Einzelförderung

Projektleitung der Universität Münster

Müller-Olm, Markus

Antragsteller*innen der Universität Münster

Müller-Olm, Markus

Wissenschaftliche Projektmitarbeiter*innen der Universität Münster

Wenner, Alexander

Projektbeteiligte Organisationen außerhalb der Universität Münster

  • Technische Universität München (TUM)Deutschland

Projekte der vorangehenden Förderperiode

Laufzeit: 20.09.2007 - 30.11.2012 | 1. Förderperiode
Gefördert durch: DFG - Sachbeihilfe/Einzelförderung
Art des Projekts: Gefördertes Einzelprojekt

Publikationen der Universität Münster entstanden im Projekt

Mantel Heiko, Müller-Olm Markus, Perner Matthias, Wenner Alexander (2015)
In: Falaschi Moreno (Hrsg.), Logic-Based Program Synthesis and TransformationSpringer International Publishing. doi:10.1007/978-3-319-27436-2_12
Forschungsartikel in Sammelband (Konferenz) | Peer reviewed | Veröffentlicht
Lammich Peter, Müller-Olm Markus, Seidl Helmut, Wenner Alexander (2013)
In: Francesco Logozzo, Manuel Fahndrich (Hrsg.), 20th Static Analysis Symposium477-498Springer.
Forschungsartikel in Sammelband (Konferenz) | Peer reviewed | Veröffentlicht