Logik & Formale Verifikation

Logik & Formale Verifikation

Wie kann die Korrektheit von Software und Hardware formal überprüft werden? Wie können Datenbankanfragen schneller beantwortet werden? Wie kann Wissen so gespeichert werden, dass es leicht genutzt werden kann? 

Bei der Beantwortung solcher Fragen spielen formale Methoden aus der Logik eine große Rolle.

Schwerpunkte

Der Forschungsbereich Logik und Formale Verifikation rund um Prof. Dr. Thomas Zeume wendet logische Methoden auf Problemstellungen der Informatik an. Es werden effiziente Algorithmen für in Anwendungen auftretende Logiken entwickelt und die Ausdruckskraft von solchen Logiken untersucht.

Effiziente Anfrageauswertung für dynamische Datenbanken. Das Extrahieren von Informationen aus riesigen Datenmengen, die häufig aktualisiert werden, ist in vielen Disziplinen eine große Herausforderung. Die dynamische Komplexitätstheorie untersucht die theoretischen Grundlagen von logischen Anfragesprachen für Datenbanken, die häufigen Änderungen unterworfen sind. Eines der Hauptziele in diesem Bereich ist die Entwicklung einer Theorie zur Klassifizierung von Abfragen in Bezug auf die Menge an Ressourcen, die für ihre dynamische Auswertung benötigt werden.

  • Die Forschung befasst sich mit der Entwicklung von Methoden zur Untersuchung des Ressourcenbedarfes zur Aufrechterhaltung von Anfragen in dynamischen Kontexten.

Logik für Spezifikation und Verifikation. Die automatisierte Verifikation von Software und Hardware ist eine wichtige Aufgabe. Oft werden beabsichtigte Eigenschaften eines Systems durch logische Formalismen spezifiziert. Ähnliche Formalismen sind die Grundlage für Anfragesprachen zum Extrahieren von Informationen aus baumartigen Daten und Graphdatenbanken.

  •  Das Team untersucht logische Systeme im Hinblick auf ihre Anwendbarkeit als Spezifikations- und Verifikationssprachen.

Webbasierte Lehre im Bereich Formale Methoden. Eine typische Anwendung von Logik in der Informatik ist die Modellierung von Szenarien mithilfe logischer Formeln und das Schlussfolgern neuen Wissens aus einer solchen Modellierung.

  •   Entwickelt wird ein interaktives, webbasiertes Lehrsystem zur Unterstützung Studierender beim Lernen der nötigen formalen Grundlagen.