Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2016/17 / Design und Verifikation paralleler und nebenläufiger Algorithmen


Inhaltsbereich

Design und Verifikation paralleler und nebenläufiger Algorithmen

Seminar, Hofmann, Cichon, Jost, Schöpp

Aktuelles

  • Die Vorbesprechung mit Themenvergabe findet am Montag, den 07.11. von 14 bis 15 Uhr im Raum L109, Oettingenstr. 67 statt.
  • Die Anmeldung erfolgt über die Zentralanmeldung für Bachelorseminare auf UniWorx.

Inhalt

Dieses Seminar beschäftigt sich mit Methoden des Entwurfs und der Verifikation nebenläufiger Programme. Für nebenläufige Programme sind formale Analyse und das methodische Vorgehen bei der Entwicklung von besonderer Bedeutung, da Nebenläufigkeit das systematische Testen erschwert. In diesem Seminar betrachten wir verschiedene Möglichkeiten der Verifikation nebenläufiger Algorithmen, wie zum Beispiel Owicki und Gries' Erweiterung der Hoare Logik oder die Rely-Guarantee-Methode. Darüber hinaus beschäftigen wir uns mit Möglichkeiten, den Entwurf nebenläufiger Algorithmen zu unterstützen. Dies beinhaltet zum Beispiel programmiersprachliche Primitive für Nebenläufigkeit, algorithmische Patterns sowie die Implementierung nebenläufiger Datenstrukturen.


Themen

Die Vortragsthemen werden in einer Vorbesprechung zu Beginn des Semesters vergeben.

 


Organisation

Anforderungen

  • Blitzvortrag 90 Sekunden: Inhaltsübersicht, eine Folie
  • Vortrag: 30 Minuten (plus Diskussion)
  • Anwesenheit während der Seminarsitzungen
  • Ausarbeitung zum Thema
    • 7.000-14.000 Zeichen bei Bachelor Studenten
    • 20.000-30.000 bei Master- und Diplomstudenten

Zeit und Ort

  • Zeitplan und Themen werden in einer Vorbesprechung zu Semesterbeginn mit den Teilnehmern festgelegt.
  • Blitzvorträge: Montag, 21.11.2016, 13:45 (pünktlich!)
  • Abgabe Ausarbeitung (Vorabversion): bis 21.12.2016 per UniWorX abgeben
  • Abgabe Reviews: bis 18.1.2017 per UniWorX abgeben
  • Seminar: Montag, 20.02.2017, 9:00 Uhr c.t. bis ca. 18:00 Uhr
  • Abgabe Ausarbeitung (Endfassung): 27.02.2017

 


Themen

  1. Owicki, Gries: An axiomatic proof technique for parallel programs I. [Bostelmann, Betreuer: MH]
  2. Coleman, Jones: A structural proof of the soundness of rely/guarantee rules. [Özdemir, Betreuer: US]
  3. Vafeiadis: Concurrent separation logic and operational semantics. [Steinecker, Betreuer: SJ]
  4. Brookes: Full abstraction for a shared-variable parallel language. [von Raven, Betreuer: US]
  5. Turon: Reagents: Expressing and Composing Fine-grained Concurrency. [Betreuer: US]
  6. Benton, Cardelli, Fournet: Modern Concurrency Abstractions for C#. [Kiermeier, Betreuer: GC]
  7. White: Hadoop the Definitive Guide. [Betreuer: MH]
  8. Pregel: A System for Large-Scale Graph Processing. [Leffers, Betreuer: MH]
  9. Single Assignment C (www.sac-home.org). [Hof, Betreuer: SJ]
  10. Bronson: A Practical Concurrent Binary Search Tree. [Westphal, , Betreuer: GC]
  11. Howard: Relativistic Red-Black Trees. [Seidl, Betreuer: SJ]

 


Weitere Informationen

Tipps zum Aufbau von Vorträgen und zu Präsentationstechniken:

 

Artikelaktionen


Funktionsleiste