Uni des Saarlandes
Informatik
Programmiersysteme
Vorlesungen
LSV SS-02


Hauptseite
Termine
Literatur
Übungen
Klausuren
Mailingliste
Software
Skript

Skript: Logik, Semantik und Verifikation

Das Skript begleitet die Vorlesung und hält die wichtigsten Inhalte fest. Es wird vorlesungsbegleitend geschrieben, aufbauend auf der Version vom letzten Jahr. Neben dem Skript sollten Sie unbedingt noch weitere Literatur studieren, da das Skript in Bezug auf Motivation und Abdeckung noch unvollständig ist.

Logik, Semantik und Verifikation
Eine Einführung für Informatiker
Version SS 2002
Gert Smolka

• Vorwort (ps, pdf)
• 1 Mathematische Objekte (ps, pdf)
• 2 Strukturelle Rekursion und Induktion (ps, pdf)
• 3 Syntax und Semantik von arithmetischen Ausdrücken (ps, pdf)
• 4 Aussagenlogik (ps, pdf)
  • Bryant's Originalpapier über OBDDs
• 5 Fixpunktoperatoren (ps, pdf)
• 6 Programme mit Schleifen (ps, pdf)
• 7 Formeln mit Quantoren (ps, pdf)
• 8 Programmverifikation (ps, pdf)
• 9 Berechenbarkeit (ps, pdf)
• 10 Elementare Typtheorie (ps, pdf)