Seminar Werkzeuge zur vollautomatischen Analyse von Programmen

Deadline zur Anmeldung und Vorbesprechung: Dienstag 10. Mai 2011, 14:00 Uhr, Raum 3018 N

Inhalt:

Die Modellierung kritischer Software (z.B. in Automobilen, Zugsteuerungen oder in der Flug- und Raumfahrt) mit Hilfe von Sprachen, die eine formale Semantik besitzen, erlaubt eine präzise Analyse von Eigenschaften der zugrundeliegenden Systeme. Dadurch können Fehler frühzeitig erkannt und ausgebessert werden, was zu einer Reduzierung der Kosten- und Sicherheitsrisiken eines Softwareprojekts beiträgt. Dazu werden diverse Modellierungs- und Verifikationstechniken vermehrt auch in der Industrie eingesetzt.

In letzter Zeit werden vollautomatische Tools immer populärer und diese können auch immer schwierigere Probleme lösen. Das Seminar soll eine anwendungsorientierte Einführung geben zu einigen vielversprechenden Tools aus den Bereichen

• Model Checking
• Automatisches Theorembeweisen
• Abstrakte Interpretation

Anforderungen:

• Selbständige Erarbeitung der Literatur und Einarbeitung in das jeweilige Tool.
• Schriftliche Ausarbeitung eines Berichts (ca. 12 Seiten LNCS-Style).
• Ausarbeitung und Halten einer Präsentation (45min Vortrag und Diskussion).
• Aktive Teilnahme an den Vorträgen der anderen Teilnehmer.

Achtung: Das Seminar ist für Master- und Diplomstudenten und kann nicht im Bachelor belegt werden.

Termine:

• Vorbesprechung: Dienstag, 10. Mai 2011, 14:00 Uhr, Raum 3018 N

Anmeldung:

• Ab sofort per Email (Betreff 'Anmeldung Seminar automatische Programmanalyse') an Gidon Ernst unter Angabe des Namens, Studiengangs, der Matrikel-Nr. und einem Wunschthema (first come first serve).
• Deadline: in der Vorbesprechung

Themen:

Alle Vorträge sollen Tools zur Modellierung, Programmierung oder Verifikation von Softwaresystemen vorstellen und anhand von Beispielen demonstrieren.

 

1. Dafny: Automatische Verifikation von objektorientierte Programmen. Basiert auf den Tools Boogie und Z3 von Microsoft.
2. Chalice: Analyse von Nebenläufigen Programmen mit Hilfe des Ownership-Konzepts. Basiert ebenfalls auf Boogie und Z3.
3. Alloy/Kodkod: Ein Tool zur vollautomatischen Suche nach Fehlern in Spezifikationen und Programmen.
4. TVLA: TVLA basiert auf Shape Analysis, einer vollautomatischen Technik zum Nachweis von Eigenschaften von Datenstrukturen im Heap, wie z.B. Bäume oder Liste. U.a. werden auch nebenläufige Programme unterstützt.
5. JStar: Ein automatisches Verifikationstool für objekt-orientierte Java-Programme, das auf Separation Logic und Abstrakter Interpretation beruht.
6. Die Themenliste wird bei Bedarf erweitert

Ablauf:

1. Teilnahme an der Vorbesprechung und Einführung (Teilnahme ist Pflicht).
2. Erste Themenbesprechung mit dem Betreuer; dieser gibt evtl. Literatur zum Thema heraus.
3. Erstellung der Ausarbeitung unter Absprache mit dem Betreuer.
4. Erstellung des Vortrags unter Absprache mit dem Betreuer.
5. Abgabe der Endversion des Berichts und der Präsentation bis spätestens zwei Tage vor der Veranstaltung.
6. Präsentation und aktive Teilnahme an den Vorträgen.

Ansprechpartner:

• Gidon Ernst, Tel.: 0821 / 598-2183, Zimmer 3043 N

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung:	Hauptstudium
Fachrichtung Lehrveranstaltung:	Informatik
Nummer der Lehrveranstaltung:	07117
Dauer der Lehrveranstaltung:	2 SWS
Typ der Lehrveranstaltung:	S - Seminar
Leistungspunkte:	4 LP
Bereich:	Softwaretechnik und Programmiersprachen
Prüfung:	Referat / Hausarbeit
Semester:	SS 2011