Dozent:	Dirk Nowotka
Zeit und Ort:	Mo 09:45-11:15 im Raum V38.04
	Do 11:30-13:00 (14-tägig) im Raum V38.02
	Montagstermine 2009: 19.10., 26.10., 2.11., 9.11., 16.11., 23.11., 30.11., 7.12., 14.12., 21.12.
	Donnerstagstermine 2009: 22.10., 5.11., 19.11., 03.12., 17.12.
	Montagstermine 2010: 11.01., 18.01., 25.01., 01.02., 08.02., 15.02.
	Donnerstagstermine 2010: 14.01., 28.01., 11.02.
Übungen:	Do 11:30-13:00 (14-tägig) im Raum V38.02
Hörerkreis:	Studenten im Hauptstudium der Diplomstudiengänge Informatik und Softwaretechnik
Inhalt:	Entwickler im industriellen Bereich sind zwischen 50% und 70% der Zeit mit der Fehlererkennung und Fehlerkorrektur im neuen Code beschäftigt. Trotz dieses Aufwands ist die mangelnde Zuverlässigkeit vom Code eines der größten Probleme der Softwareindustrie. Wie Robert X. Cringely sagte: ``If the automobile had followed the same development cycle as the computer, a Rolls-Royce would today cost $100, get a million miles per gallon, and explode once a year, killing everyone inside''. Zunächst werden Testing-Techniken präsentiert. Begriffe und Verfahren für systematisches Testen werden eingeführt: inspections, walkthroughs, control-flow coverage, data-flow coverage, black-box und white-box testing, test suites, conformance testing. Im zweiten Teil der Vorlesung werden Model-Checking-Verfahren für die automatische Programmverifikation behandelt. Zunächst wird die Problematik der Programmmodellierung erklärt und die temporale Logik CTL als formale Spezifikationssprache präsentiert. Anschließend werden enumerative und symbolische Model-Checking-Algorithmen beschrieben. Der dritte und letzte Teil der Vorlesung ist der Datenflussanalyse gewidmet. Die zugrundeliegende Theorie der Abstrakten Interpretation wird beschrieben, ebenso wie Anwendungen in den Bereichen Zuverlässigkeit und Code-Optimierung.
Übungen:	Blatt 1, Lösungen 1 Blatt 2
Folien:	[PDF] (von Prof. Esparza)