Logik und Verifikation

Beschreibung

Dieser Kurs befasst sich mit logikbasierten formalen Methoden und wie man sie zur Verifikation in der Informatik einsetzt.
Es werden die Sprache und die Semantik der Sentenzenlogik (SL) und der Logik erster Ordnung (FOL) genau definiert.
Wir führen den Begriff des Modells ein und zeigen, wie Hardware- und Softwaresysteme in diesem Rahmen modelliert werden können. Wir betrachten auch
semantische Folgerung vs. syntaktische Ableitbarkeit von Formeln und wie diese beiden Begriffe durch Korrektheit und Vollständigkeit miteinander verbunden sind. Vollständigkeit wird für SL formal bewiesen und für FOL ausführlich diskutiert (in Form von Vollständigkeit der Widerlegung).
Beide Logiken werden auf wichtige Verifikationsprobleme angewandt: SL und seine Erweiterung LTL zur Verifikation linearer zeitlicher Eigenschaften in nebenläufigen Systemen, und
FOL zur Verifikation von Eingabe/Ausgabe-Eigenschaften von Programmen (Hoare-Kalkül).
Wir zeigen, wie das Auflösungskalkül für FOL zu PROLOG führt, einer Programmiersprache, die auf FOL basiert.
Wir zeigen auch, dass SL zu einer deklarativen Version von PROLOG führt: Answer Set Programming (ASP), die zur Lösung von Problemen verwendet werden kann, die sich auf der zweiten Ebene der Polynomhierarchie ausdrücken lassen.
Obwohl ASP keine vollwertige Programmiersprache ist, kann sie für viele natürlich auftretende Probleme verwendet werden und erlaubt es, diese auf eine rein deklarative Weise zu modellieren.

1. Einführung
2. Sententielle Logik (SL)
3. Verifikation I: Reaktive Systeme
4. Logik erster Ordnung (FOL)
5. Verifikation II: Hoare-Kalkül
6. Von FOL zu PROLOG
7. PROLOG

Übersetzt mit DeepL.com (kostenlose Version)

Vorlesungsaufzeichnungen