Seminar "Programmverifikation"

4.1.23 S2 c Inf CV

Seminar im Wintersemester 2006/07

Jun.-Prof. Dr. Bernhard Beckert (BB)
Christoph Gladisch (CG)
Angela Wallenburg (AW)
Dr. Manfred Kerber (MK)

Aktuelles

23.01.07: Am 08.02. findet das Seminar ausnahmsweise in Raum F522 statt.
27.10.06: Einen anderen Raum zu finden, gestaltet sich schwierig. Bis auf weiteres bleiben wir in E016.
26.10.06: Die Anmeldung über MeToo ist abgeschlossen. Alle Themen sind vergeben.
16.11.06: Kein Seminartreffen
23.11.06: Dreiminutenvorträge. Schicken Sie Ihre Folien im pdf-Format rechtzeitig an Ihren Betreur. Benennen Sie die Datei nach dem Schema: KurzNachnameVorname

Ort und Zeit

Das Seminar findet Donnerstags, 12 Uhr c.t. in E016 statt.

Die nächsten Termine

Do 25.01.07, 12 Uhr c.t.: Der 9. und 10. Vortrag
Do 18.01.07, 12 Uhr c.t.: Der 7. und 8. Vortrag

Vortragsthemen

Thema (Seminarteilnehmer,Betreuer)

The Verification System ACL2 (Robert Menzel, AW)
Light-weight Formal Methods: The Alloy Method (Volker Klasen, AW)
The B Method (Christian Diefenthal, AW)
Finding Loop Invariants by Static Program Analysis (Markus Bender, AW)
Finding Loop Invariants by Dynamic Program Analysis: The DAIKON Tool (Stephan Sonntag, CG)
Structural Test Coverage Criteria (Sebastian Ebertz, CG)
Fault- and Error-based Test Coverage Criteria (Thomas Pilz, CG)
Bounded Symbolic Execution: The Bogor/Kiasan Tool (Martin Schnorr, CG)
Combining Verification and Testing: Microsoft Research's Yogi Tool (Joachim Pehl, CG)
Combining Symbolic Porgram Execution and Testing: Microsoft Research's MUTT Tool (Daniel Schaaf, CG)
Inductionless Induction (Jürgen Starek, BB)
Testing Concurrent and Distributed Systems (Alexander Rostilov, BB)
Shape Analysis und Separation Logic (Matthias Gerz, BB)
Zusatzthema 1 (Michael Juszczak, MK)
Zusatzthema 2 (Kai Brüggemann, MK)

Allgemeine Informationen

Die Vorträge können in Deutsch oder Englisch gehalten werden (bei einigen der Themen ist ein Vortrag auf Englisch erw&unscht;).

Lernziele sind bei diesem, wie bei jedem anderen Seminar:

Selbständiges Erarbeiten eines vorgegebenen Themas
Vorbereiten und Halten eines Fachvortrags
Auseinandersetzung mit und Diskussion über Fachvorträge

Organisatorisches

Teilnehmer

Bis zu 12 Teilnehmer.

Anmeldung

Die Anmeldung erfolgt über MeToo. An diejenigen, die sich angemeldet haben, werden die Seminarplätze vorrangig vergeben (in der Reihenfolge der Anmeldung). Da aber erfahrungsgemäß nicht alle, die sich angemelden, auch teilnehmen, besteht durchaus auch für diejenigen die Chance noch teilzunehmen, die sich nicht angemeldet haben. Wer Interesse hat teilzunehmen ohne sich angemeldet zu haben, sollte zur Vorbesprechung kommen.

Wer sich angemeldet hat aber an der Vorbesprechung nicht teilnimmt, läuft Gefahr seinen Platz zu verlieren.

Zeitplan

Vorbesprechung und Themenvergabe in der 1. Vorlesungswoche
Einführungsveranstaltung "Programmverifikation" in der 2. Woche
Einführungsveranstaltung "Wie erarbeite und halte ich einen Vortrag?" in der 3. Woche
Ein Draft der Vortrags (vollständiger Foliensatz) muss spätestens zwei Wochen vor dem jeweiligen Vortrag stehen..
Die Ausarbeitung (10 Seiten) muss bis Vorlesungsende fertig sein.
Die Termine für die Vorträge werden bei der Vorbesprechung vereinbart.

Voraussetzungen zur Erlangung des Scheins

Halten (in freier Rede) eines selbständig und sorgfältig erarbeiteten Vortrags von ca. 35-45 Minuten mit anschließender Diskussion.
Anwesenheit bei den Seminarvorträgen und Beteiligung an der Diskussion nach den Vorträgen.
Anfertigung einer Ausarbeitung zum Thema des Vortrags von ca. 10 Seiten. Wie bei wissenschaftlichen Konferenzen üblich soll hierfür der LNCS-Style des Springer-Verlags verwendet werden. Formatvorlagen für LaTeX und MS Word können von der Springer-Webseite heruntergeladen werden. Nutzer von MS Word müssen ihre Ausarbeitung als PostScript oder PDF einreichen. Wir empfehlen die Verwendung von LaTeX. Eine Einführung in LaTeX finden sie hier.

LaTeX

Für die Erstellung der Folien sei das prosper-Package empfohlen.

Bernhard Beckert