Programmiermethodik

Wir über uns

Die Erstellung korrekter Software ist ein zentrales Anliegen der Informatik. Fehlerhafte Software verursacht große wirtschaftliche Schäden, von denen nur die spektakulärsten einer breiteren Öffentlichkeit bekannt werden. Folgerichtig gewinnt die Entwicklung korrekter Programme auf Grundlage formaler Spezifikationen und mathematischer Beweise zunehmend an Bedeutung. Zum industriellen Einsatz sind dabei Programmverifikationssysteme erforderlich, denn die Komplexität realer Anwendungsprogramme schließt eine manuelle Verifikation von vornherein aus.

Darüber hinaus sind mit der stetig anwachsenden Bedeutung von Anwendungen und Diensten im Rahmen offener Kommunikationsnetze (e-commerce, virtuelle Unternehmen, der Austausch von Informationen über das Internet usw.) die Sicherheit und Verlässlichkeit von Programmen, Protokollen und Netzwerkstrukturen für die zukünftige Informationsgesellschaft von entscheidender Bedeutung.

Das Fachgebiet Programmiermethodik der TU Darmstadt stellt diese für die moderne Informatik aber auch für eine wirtschaftlich erfolgreiche Nutzung zentralen Fragestellungen in das Zentrum seiner Forschung.

Dabei folgen wir der Leitidee, dass eine systematische und logikbasierte Formalisierung von Spezifikationen und Anwendungsszenarien und der mathematisch fundierte Beweis relevanter Programm- und Modelleigenschaften erforderlich sind, einen entscheidenden Beitrag zur Erhöhung der Korrektheit von Software und der Sicherheit von verteilten Anwendungen in offenen Netzen zu liefern.

Aus diesem Ansatz resultieren unterschiedliche konkrete Fragestellungen, mit denen sich das Fachgebiet Programmiermethodik beschäftigt. Dazu zählen:

  • der (formale) Nachweis der Korrektheit und Zuverlässigkeit funktionaler und imperativer Programme
  • die Betrachtung der Sicherheit und Verlässlichkeit von Protokollen
  • die Modellierung und Formalisierung von Bedrohungsszenarien und Sicherheitseigenschaften im Kontext verteilter Anwendungen und kryptographischer Protokolle
  • die Entwicklung von Verfahren und Systemen zur rechnergestützten Verifikation
  • die Integration von Lernverfahren in Beweissysteme
  • die Untersuchung menschlicher Problemlösungs-Strategien, um diese für (automatische) Verifikationswerkzeuge nutzbar zu machen
  • die Analyse der Terminierung von Programmen

Die geschilderten Aktivitäten finden auch in den angebotenen Lehrveranstaltungen eine Entsprechung. Studenten haben die Möglichkeit, in Vorlesungen und Übungen die Grundlagen unserer Forschungsgebiete zu erlernen, in Seminaren aktuelle Fragestellungen und neue Ansätze zu erfahren und in Praktika und Studienarbeiten moderne und industriell eingesetzte Werkzeuge kennen zu lernen und an deren Weiterentwicklung beteiligt zu sein.