6.0/4.0 VO Formale Methoden der Informatik (185.291)

Lehrveranstaltungsleiter: Uwe Egly, Bernhard Gramlich, Reinhard Pichler, Gernot Salzer, Hans Tompits

Diese Lehrveranstaltung ist eine Basislehrveranstaltung der Masterstudien Computational Intelligence, Computergraphik & Digitale Bildverarbeitung, Information & Knowledge Management, Medieninformatik, Medizinische Informatik, Software Engineering & Internet Computing sowie Technische Informatik (siehe Master-Studienpläne).

• Aktuelles
• Inhalt und Lehrziel
• Lehrveranstaltungstermine
• Unterlagen
• Beurteilung
• Prüfungstermine
• Prüfungsergebnisse
• Alte Prüfungsangaben

Aktuelles

• Nächster Prüfungstermin (zum WS 2009/2010): Freitag, 19.3.2010, 12:00-14:00, EI 7
  Anmeldung über TUWIS++ zwischen 5.3. und 18.3.2010 erforderlich.
  Erlaubte Prüfungsunterlagen: Alle im WS 2009/2010 zur Verfügung gestellten Dokumente ausgenommen Übungsblätter, alte Prüfungsangaben und Musterlösungen dazu. Keine handschriftlichen Unterlagen.

• Was TUWIS++ zu dieser Lehrveranstaltung sagt.

Inhalt und Lehrziel

Inhalt   Prädikatenlogik als Spezifikationssprache, Wiederholung prädikatenlogischer Konzepte; Grundlagen der formalen Programmverifikation und der formalen Programmsemantik; Spezifikation und Verifikation mit angewandten Logiken (wie Modallogiken und CTL); Komplexitätstheorie: Problemreduktion, polynomielle Hierarchie, Erläuterung der wichtigsten TIME- und SPACE-Klassen.

Lehrziel   Schulung des abstrakten, formalen und logischen Denkvermögens sowie die Vermittlung formaler Methoden der Informatik.

Lehrveranstaltungstermine

Siehe TUWIS++.

Unterlagen

Die Lehrveranstaltung orientiert sich großteils an folgendem Lehrbuch:

Michael R. A. Huth, Mark D. Ryan. Logic in Computer Science – modelling and reasoning about systems.
427 pages, 2nd edition, Cambridge University Press, 2004, ISBN 0-521-54310-X paperback
www.cs.bham.ac.uk/research/lics

Folien (im PDF-Format) werden im Laufe des Semesters hier zur Verfügung gestellt:

• Block 1: Predicate logic as specification language, Natural Deduction, SAT (8.3.-24.3.2010, Uwe Egly)
  • Propositional logic (reminder) (2x2)
  • Syntax and semantics of first-order logic (2x2)
  • Exercises I (Propositional logic)
  • Specifying with first-order logic (2x2)
  • Natural deduction (2x2)
  • Exercises II (First-order logic and natural deduction)

• Block 2: Formal Verification of SW (Hoare calculus) (12.4.-26.4.2010, Gernot Salzer)

• Block 3: Formal Verification of HW: BDDs, computation tree logic, linear-time temporal logic (28.4.-12.5.2010, Bernhard Gramlich)

• Block 4: Modal Logic (17.5.-2.6.2010, Hans Tompits)

• Block 5: Complexity theory: reductions, classes, undecidability (7.6.-21.6.2010, Reinhard Pichler)

Alte Unterlagen (nur für Prüfungen zum angegebenen Semester empfohlen): WS 2009

Beurteilung

Der Übungsanteil der Lehrveranstaltung findet integriert in den Vorlesungsteil statt, ergänzt durch außerhalb der Vorlesungszeiten zu bearbeitende Aufgaben. Dabei wird der vermittelte Stoff anhand von Beispielen vertieft und illustriert. Die Beurteilung erfolgt durch eine schriftliche Prüfung am Ende des Semesters bzw. im Folgesemester.

Prüfungstermine

Für die Prüfungen ist eine Anmeldung über TUWIS++ erforderlich. Die Anmeldefrist beginnt zwei Wochen vor der Prüfung und endet einen Tag vor der Prüfung.

Termine: siehe TUWIS++.

Einsichtnahme jeweils: In der Sprechstunde von Gernot Salzer, Favoritenstr. 9, 3.Stock, E185/2, siehe hier.

Erlaubte Prüfungsunterlagen: Alle auf dieser Webseite zur Verfügung gestellten Dokumente ausgenommen Übungsblätter und alte Prüfungsangaben sowie Musterlösungen zu den Übungsblättern und alten Prüfungsangaben. Keine handschriftlichen Unterlagen!

Prüfungsergebnisse

Siehe TUWIS++.

Siehe auch die Notenstatistik.

Alte Prüfungsangaben