Formale Systeme und Methoden (WiSe 2011/12)
| Typ: | Seminar | ||
|---|---|---|---|
| Semester: | WS 11/12 | ||
| Zeit: | Blockveranstaltung am Semesterende |
||
| Dozierende: |
Prof. P. H. Schmitt Prof. Bernhard Beckert Thorsten Bormer Daniel Bruns David Faragó Dr. Christoph Gladisch Christoph Scheben Mattias Ulbrich |
||
| SWS: | 2 | ||
| LVNr.: | 24353 | ||
| Hinweis: | Weiterführendes Seminar für Diplom- oder Master-Studierende |
||
Details zur Veranstaltung
Software-basierte Systeme sind aus unserem Alltag nicht mehr wegzudenken. Sie halten Einzug in nahezu alle Bereiche unseres Lebens. Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung nur allzuoft auf der Strecke. In manchen Bereichen mag dies tolerierbar sein, sobald aber durch fehlerhafte Software Menschenleben gefährdet sind (z. B. Eisenbahnwesen oder Anwendungen in der Medizin) oder hohe finanzielle Schäden zu befürchten sind (z. B. Internet-Banking), muss auf die Qualität - insbesondere auf die Korrektheit - der Software besonderer Wert gelegt werden.
Deswegen gibt es umfangreiche Forschung zu (formalen) Methoden, deren Anwendung es tatsächlich ermöglicht, fehlerfreie Software zu entwickeln oder zumindest die Qualität der Software deutlich zu erhöhen. In diesem Seminar wird eine Auswahl an aktuellen Ergebnissen aus dieser Forschung vorgestellt.
Die Seminarteilnehmer bereiten unter Anleitung durch einen Betreuer einen Vortrag zu einem dieser Forschungsergebnisse vor. Ziel ist, dass der Vortragende selbst sich ein gründliches Verständnis des Themas erarbeitet und dem Auditorium in der Kürze der zur Verfügung stehenden Zeit die wesentlichen Informationen und Einsichten vermittelt.
Organisatorisches
Die Veranstaltung richtet sich an Studierende im Master- bzw. fortgeschrittenen Diplom-Studium. Kenntnisse aus den Vorlesungen "Formale Systeme" und "Softwaretechnik" werden als bekannt vorausgesetzt. Die Prüfungsleistung besteht aus einem 45-minütigen Vortrag und einer schriftlichen Ausarbeitung. Vorträge und Ausarbeitungen können in deutsch oder englisch erstellt werden.
Eine Vorbesprechung der Themen findet nicht statt. Zur Anmeldung benutzen Sie bitte unten stehendes Formular bis Sonntag, 23. Oktober unter Nennung des gewünschten Themas (eventuell Zweitwunsch). Die Themen werden nach dem Prinzip "first-come/first-serve" verteilt. Ihr Betreuer wird sich daraufhin mit Ihnen in Verbindung setzen. Für weitere organisatorische Fragen wenden Sie sich bitte an Daniel Bruns.
Zur inhaltlichen Vorbereitung wird es voraussichtlich am 17. November um 11:30 in SR 301 einen Termin mit Kurzvorträgen geben. Dort stellen Sie in 5 Minuten (max. 5 Folien!) die Gliederung Ihres Hauptvortrages dar.
Das eigentliche Seminar selbst findet als Blockveranstaltung am Semesterende zusammen mit dem Seminar "Bugfinding Techniques" der Gruppen von Jun.-Prof. Taghdiri und Dr. Sinz statt. Es findet am 10. Februar von 14 Uhr bis 16:30 Uhr in Raum -120 im Informatikgebäude statt. Die Abgabe der Ausarbeitungen ist für die darauffolgende Woche vorgesehen.
| Titel | Betreuer |
|---|---|
| Verifikation eines Microkernels | Thorsten Bormer |
| Temporallogische Laufzeitprüfung | Daniel Bruns |
| Zugriffskontrolle mit "fractional permissions" | Daniel Bruns |
| When BDDs Fail: Conformance Testing with Symbolic Execution and SMT solving | David Faragó |
| Coverage-based test case generation | David Faragó |
| Engineering DPLL(T) + Saturation | Christoph Gladisch |
| Riding the Roller Coaster of Information-Flow Control Research | Christoph Scheben |
| Tracking Information Flow in Dynamic Tree Structures | Christoph Scheben |
| Paralocks - Role-Based Information Flow Control and Beyond | P. H. Schmitt |
| Local Reasoning and Dynamic Frames for the Composite Pattern | P. H. Schmitt |
| HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler | Mattias Ulbrich |
Online-Anmeldung
Material
Tips für gute Seminarvorträge
LaTeX-Vorlagen
Die Erstellung der Ausarbeitung erfolgt verpflichtend in LaTeX unter Benutzung der IEEE-Transactions-Vorlage. Sie ist in den gängigen LaTeX-Distributionen enthalten (TeX Live: IEEEtran, MiKTeX: ieeetran). Zum Benutzen beginnen Sie Ihr Dokument mit "\documentclass[a4paper]{IEEEtran}".