Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Verification of a Distributed Floodfill Implementation

Typ: MA
Datum: 2018-07-10
Betreuer: Mattias Ulbrich
Bearbeiter:
Aushang:

Beim wissenschaftlichen Rechnen sind heutzutage Parallelisierung und Optimierung zunehmend wichtige Techniken, die garantieren, dass trotz der Abschwächung von Moore's Law weiterhin bei intensiven Rechenaufgaben skaliert werden kann. Dabei werden die Implementierungen immer effizienter, komplexer und weniger verständlich. Es schleichen sich leichter Fehler ein. Formale Methoden können helfen, Fehler in optimierten Implementierungen zu entdecken und zu beheben. Sie könenn auch benutzt werden, um zu zeigen, dass bestimmte Fehlerklassen nicht auftreten.

In Zusammenarbeit mit dem IAM-CMS am KIT wollen wir speziell für einen verteilten Floofill-Algorithmus zeigen, dass dieser korrekt und deadlockfrei funktioniert.

Dazu gilt es, das Problem zunächst genau zu analysiseren, eine geeignete Abstraktion zu finden, diese in Logik zu kodieren und mittels eines automatischen Modelcheckers zu verifizieren.

Your Profile

Basic knowlegde of predicate logic, specification and calculi, as e.g. taught in the Formal Methods (Formale Systeme) course at KIT, is required.