Pflichtveranstaltungen

Lehrinhalte:
Syntax und Semantik der Aussagenlogik, funktionale Vollständigkeit und Normalformen, Kompaktheitssatz der Aussagenlogik, vollständige Beweiskalküle: Resolution und ein Sequenzenkalkül;

Syntax und Semantik der Logik erster Stufe, Strukturen und Belegungen, Normalformen und Skolemisierung, der Satz von Herbrand und der Kompaktheitssatz der Logik erster Stufe, vollständige Beweiskalküle: (Grundinstanzen-)Resolution und ein Sequenzenkalkül,
Gödelscher Vollständigkeitssatz, Unentscheidbarkeit der Logik erster Stufe;

optional: Exkurse zu Ausdrucksstärke und model checking

Modellierung nebenläufiger Software mit der Sprache ProMeLa, Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik, Theoretische Grundlagen von Modellprüfungsverfahren, Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN, Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe, Grundlagen der kontraktbasierten Softwarespezifikationssprache JML, Dynamische Logik als eine Programmlogik erster Stufe, Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen, Werkzeugunterstützte Verifikation von Java-Programen mit der KeY System