Formale Methoden der Softwaretechnik II
Willkommen auf der Heimatseite der Lehrveranstaltung "Formale Methoden der Softwaretechnik II" im Sommersemester 2006!
Inhaltliches
Diese Veranstaltung ist eine Vertiefung der Verstanstaltung Formale Methoden der Softwaretechnik I vom letzten Semester. Inhalt der Veranstaltung sind damit weiterhin die formale Methoden, d.h. auf der Mathematik (speziell formaler Logik) basierende Methoden zur Sicherstellung der Korrektheit von Software.
Im Gegensatz zum ersten Teil, der einen breiten Überblick über die verwendeten Methoden sowie einen Einblick in die theoretischen Grundlagen geben wollte, werden wir in diesem Teil zwei Aspekte in der Tiefe betrachten, nämlich die Verifikation und die korrekte Programmentwicklung.
Themen
In der Veranstaltung werden folgende Themen behandelt:- Programmverifikation:
- Floyd-Hoare-Logik (zur Wiederholung),
- Prädikatentransformer,
- Generation von Verifikationsbedingungen,
- Modellierung von imperativen Programmen,
- Verifikationswerkzeuge
- Entwicklung korrekter Programme:
- Entwicklung von korrekten Programmen durch Transformation,
- Algorithmendesign,
- Transformationswerkzeuge
Organisatorisches
VAK: 03-05-H-604.04.
Kategorie: V, ECTS: 6.
Modulbereich: Theorie
Termine:
- Vorlesung: Di 10-- 12, MZH 8090. Achtung, geänderter Termin!
- Übungen: Do 9 s.t. -- 10, MZH 6240. Am 27.04.06 findet noch keine Übung statt!
- Veranstaltungsbeginn (erste, außerplanmäßige Vorlesung): Do 20.04.2006 09:00
Achtung: Wegen starker inhaltlicher Überschneidungen kann dieses Modul nicht gleichzeitig mit dem Modul "Techniken zur Entwicklung korrekter Software II" angerechnet werden.
Voraussetzungen
Formale Methoden der Softwaretechnik I ist keine formale Voraussetzung zum Besuch der Veranstaltung, aber der zweite Teil baut natürlich auf dem Inhalt des ersten Teils auf, insbesondere den Grundlagen (formale Logik und Semantik). Diese Kentnisse können auch in anderen Veranstaltungen, z.B. Logik für Informatiker, erworben worden sein.
Vorlesungsfolien
- Alle Folien im Überblick: [PDF] (Fassung vom 18.07.06; wird ständig aktualisiert).
- Handouts pro Vorlesung (PostScript schwarz-weiß, 8 Folien auf
einer Seite, zum Ausdrucken):
- Weiteres Material:
- Der Beispielbeweis im Hoare-Kalkül aus der ersten Vorlesung.