- Methodik
- Formalismen, logische Grundlagen
- Induktion: Verifikation von funktionalen Programmen
- Temporallogik: Modellierung von nebenläufigen und verteilten Systemen
- Spezifikations- und Entwicklungstechniken
- Abstrakte Datentypen, zustandsorientierte Systeme, Z
- Nebenläufige, reaktive und verteilte Systeme
- (Horizontale) Strukturierung großer Entwicklungen und Verfeinerung
- Erzeugung effizienten Codes
Möglichkeit für Mitarbeit: Diplomarbeiten
- Deduktion
- Automatisierung der interaktiven Beweissuche
- Beweisplanung
- Anwendungs- / formalismenspezifische Heuristiken
- Wiederverwendung von Beweisen
- Sicherheit
- Korrektheitserhaltende Kalkülerweiterungen (Taktiken)
- Metalogische Beweise
- Strukturierte Deduktion
- Benutzerinteraktion
Aktuell: Implementierung
einer Beweisplanungskomponente
Möglichkeit für Mitarbeit: FoPra, Diplomarbeiten, HiWi-Tätigkeiten
- Entwicklungssysteme
- Verwaltung von Entwicklungen (Korrektheitsmanagement)
- Oberflächen
Möglichkeit für Mitarbeit: FoPra, HiWi-Tätigkeiten
- Anwendungen
- Durchführen von formalen Entwicklungen
Möglichkeit für Mitarbeit: Diplomarbeiten, HiWi-Tätigkeiten
