Verifikations- und Spezifikationsmethoden

bei Prof. Schwarz

für Master Informatik

Wintersemester 2009/10

Vorlesung:

Z2	Dienstag	13:30 - 15:00	Uhr	im Raum 202
Z2	Mittwoch	9:20 - 10:50	Uhr	im HS 4 (Tivoli)

Inhalt:

• Semantik von Programmen (denotational, operational, axiomatisch)
• Algebraische Spezifikation abstrakter Datentypen
• Hoare-Kalkül
• Model Checking

Praktikum:

Seminar zu Spezifikations- und Verifikations-Werkzeugen:

6.1.2010,	15:20 Uhr	(R311):	Meier, Winterle	pvs	(Vortrag)
			Kasimova, Scharschekeeva	HOL	(Vortrag)
			Heinicke	OBJ, Maude	(Vortrag)
20.1.2010,	15:20 Uhr	(R311):	Lasch, Schraps	Spin	(Vortrag)
			Klenner, Röschke	KeY	(Vortrag)
			Zänsler, Feuchert	SMV, NuSMV	(Vortrag)

Im Autotool gibt es jetzt einige zum Stoff der Vorlesung passende Aufgaben. Wer möchte, kann sich dort anmelden und die Aufgaben lösen.

Literaturempfehlungen:

Folien zur aktuellen Vorlesung (werden jeweils nach der Vorlesung veröffentlicht):

• 13.10.2009
• 14.10.2009
• 27.10.2009
• 28.10.2009
• 10.11.2009
• 11.11.2009, Haskell-Quelltext adt.hs, zu testen z.B. mit ghci oder hugs
• 24.11.2009
• 25.11.2009
• 8.12.2009
• 9.12.2009
• 5.1.2010
• 6.1.2010
• 19.1.2010
• 20.1.2010 (Zusammenfassung)

Im Hochschulmagazin Podium (Seiten 26/27) der HTWK Leipzig gibt es einen schönen Beitrag von Alfons Geser zur Anwendung formaler Verifikationsmethoden.

Bücher:

• Ehrich, Gogolla, Lipeck: Algebraische Spezifikation abstrakter Datentypen (Teubner 1989)
• Berard, Bidoit, et al.: Systems and Software Verification (1998)
• Baier, Katoen: Principles of Model Checking (MIT Press 2008)
• Futschek: Programmentwicklung und Verifikation (Springer 1989)
• Eveking: Verifikation digitaler Systeme (Teubner 1991)
• Nielsson, Nielsson, Hankin: Principles of Program Analysis (Springer 1999)
• Verification of Object-Oriented Software: The KeY Approach