Umfang

Dieses Thema kann als Bachelorarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute C oder C++ Kenntnisse
  • hilfreich: Prolog Kenntnisse

Problem

In ProB (Prolog) haben wir als Backend, um Prädikate zu lösen, den Z3 Solver (C/C++) eingebunden. In der Vergangenheit hatten wir aber einige Probleme damit, wie etwa, dass langsam Speicher leckt oder dass Segmentation Faults auftreten. Daher wäre es sinnvoll, Z3 in einem separaten Prozess auszuführen. Dann könnte man beispielsweise auch mehrere Instanzen starten und parallel verschiedene Prädikate lösen.

Als Technologie zur Kommunikation zwischen zwei Prozessen haben wir gute Erfahrungen mit der ZeroMQ-Bibliothek gemacht. Ihre Aufgabe in dieser Arbeit wäre daher, eine Brücke mittels ZeroMQ zwischen dem C-Interface, in dem derzeit die Prädikate zusammengebaut und gelöst werden, und einem neuen Prozess, der Z3 wrappt und die Calls weitergibt, zu schlagen.

Minimalanforderungen

  • Trennung von ProB und Z3 mittels ZeroMQ
  • Evaluation des Performance-Overheads

Erweiterungen

  • ggf. alternative Lösungsansätze

Kontakt

Philipp Körner
Raum 25.12.02.56
p.koerner@hhu.de