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