Thesis / Abschlussarbeit Recommender Systeme | Collaboration: Kooperative Konfiguration und New Work

 In
  • Abschlussarbeit Bachelor/Master
  • Karlsruhe

Webseite CAS Software AG

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.

 

Interessiert? Dann bewirb dich gleich hier

https://www.cas-mitgestalter.de/jobs/abschlussarbeit-informatik-formale-verifikation/

 

Um sich für diesen Job zu bewerben, sende deine Unterlagen per E-Mail an jobs@cas.de

Neueste Beiträge