Softwaretechnik 3, SoSe 11

Organisation

2 SWS Vorlesung, 2 SWS Übungen oder in Seminar Form.

Die Vorlesung wird in Seminarform gehalten. Das heisst es gibt Vorlesungen des Dozenten gemischt mit Seminaren der Studenten

Die Vorlesung findet Mittwochs 12:30-14:00 Uhr in 25.12.02.55 statt. Die erste Vorlesung findet Ende April statt; dort werden dann auch zusätzliche Termine ausgearbeitet.

Die erste Vorlesung findet am 27.4.2011 statt.

Spezielle Vorkenntnisse werden nicht erwartet. Man kann an dem Kurs teilnehmen auch ohne vorher "Softwaretechnik II" oder "Softwaretechnik und Programmiersprachen" gehört zu haben.

Die Veranstaltung wird in Seminarform abgehalten und beschäftigt sich damit, wie nachgewiesen werden kann, ob ein Programm korrekt funktioniert. Wir werden verschiedene Techniken und Werkzeuge betrachten, die zur Überprüfung der korrekten Funktion, der Verifikation, von Programmen dienen. Die betrachteten Programmiersprachen sind funktional und imperativ. Die Benutzten Werkzeug basieren hauptsächlich auf dem Konzept von Logic höherer Ordnung (HOL). Es sollen jeweils Grundlagen der Verifikation und der Anwendung durch ein Werkzeug studiert werden.

Als zugrunde liegender Theorembeweiser soll Isabelle benutzt werden. Auf der Isabelle Webseite befindet sich Dokumentation. Hier befinden sich Materialien einer Vorlesung über Isabelle von der ETH Zürich inklusive von Übungen mit Lösungen. Vielen Dank an Burkhart Wolff für seine Unterstützung bei der Themenauswahl.

Materialien

Folgende Artikel sollen während des Seminars bearbeitet werden:

Downloads

Retrieved from "http://www.formal-methods.de/w/Softwaretechnik_3,_SoSe_11"