Thesis / Abschlussarbeit Informatik – Formale Verifikation (Masterthesis)

Dein Thema

Das Herz unseres Produktkonfigurators Merlin CPQ ist ein inkrementeller Constraint Solver. Das Ziel des Konfigurators ist es, die Vertriebsprozesse unserer Kunden weniger fehleranfällig zu machen – dafür darf natürlich auch unser Solver keine Fehler machen. Daher möchten wir nun einen kleinen Teil unseres Solvers formal verifizieren. Hier kommst du mit der Bearbeitung deiner Masterthesis ins Spiel!

Dein Gestaltungsspielraum

  • Im Rahmen deiner Abschlussarbeit erarbeitest du eine formale Spezifikation für ein zentrales Interface unseres Constraint Solvers und verifizierst einige der Implementierungen mit einem interaktiven Theorembeweiser.
  • Um die Spezifikation des Interfaces zu extrahieren, liest du dich in hohem Detail in die Komponenten unseres Solvers ein, die das Interface verwenden.
  • Die Implementationen des Interfaces (die bis auf grundlegende Datenstrukturen keine weiteren Abhängigkeiten haben) überträgst du von Java in den Theorembeweiser.
  • Nun beweist du formal, dass die Implementierung die Spezifikation auch tatsächlich erfüllt.
  • Aus den im Beweisprozess gewonnenen Erkenntnissen leitest du Verbesserungen für die Java-Implementierung der Algorithmen ab.
  • Als Theorembeweiser verwendest du Lean, oder – auf Wunsch – ein anderes System, zum Beispiel Coq, Isabelle oder Agda.

Deine Skills

  • Du bist in der letzten Phase deines informatikorientierten Masterstudiums.
  • Du hattest bereits erste Kontakte mit dem Thema formale Verifikation und hast vielleicht sogar schon mal mit einem interativen Theorembeweiser (zum Beispiel Lean, Coq oder Isabelle) gearbeitet.
  • Du hast Interesse an Produktkonfiguration bzw. Constraint Solvern und deren praktischer Implementierung in Java.
  • Du arbeitest dich gerne in komplexe Sachverhalte ein.
  • Große Ideen entstehen nicht im stillen Kämmerlein, deshalb solltest du kommunikativ sein.
  • Für dich ist Teamgeist genauso wichtig wie für uns.

Diese Unterlagen benötigen wir vollständig von dir

  • Deine Motivation: Warum dieses Thema? Warum bei uns?
  • Zeitraum und Art (Master- / Bachelorthesis)
  • Lebenslauf
  • Aktueller Notenauszug
  • Immatrikulationsbescheinigung
  • Weitere Nachweise deiner Qualifikationen (z.B. Arbeitszeugnisse)
Die Stelle passt zu dir? Jetzt bewerben

Kontakt

Michael Berten
Referent People & WeCulture
+ 49 721 9638-550
jobs@cas.de

CAS Software AG