Weiterentwicklung von DIVE

Typ:	Hiwi
Datum:	2019-05-14
Betreuer:	Mattias Ulbrich
Aushang:

DIVE ist eine prototypische Umsetzung für ein neues Interaktionskonzepts für interaktive Programmverifikation.

Benutzer können sowohl interaktiv (mittels point-und-click und Beweis-Skripten), wie bspw. in KeY, wie auch autoaktiv (mittels Annotationen im Source-Code), wie in Dafny, Dafny-Programme verifizieren.

Dieses neue Interaktionskonzept erlaubt Benutzern nun verschiedene Sichtweisen auf das Verifikationsproblem, um die für den Benutzer geeignetste Sicht in der jeweiligen Beweissituation auszuwählen.

Ihre Aufgabe

Eine Aufgabe ist die Weiterentwicklung der neuen Oberfläche für DIVE unter der Benutzung von JavaFX (OpenJFX) und Java. Bei der Umsetzung von Benutzerinteraktionen spielt vor allem auch die intuitive Benutzbarkeit eine große Rolle.

Eine weitere mögliche Aufgabe ist Erweiterung von DIVE um neue Funktionalitäten. Bei der Weiterentwicklung von Funktionalitäten kann es von Vorteil sein, Beweisprobleme mittels DIVE zu lösen.

Beispiel

Eine Beispielaufgabe ist es eine graphische Darstellung von Aufrufabhängigkeiten umzusetzen, die der Benutzer interaktiv aktivieren kann. Die Darstellung soll, zusammen mit den weiteren Meta-Informationen, dem Benutzer helfen Querbeziehungen bei der Verifikation eines Software-Produkts zu erkennen.

Sie

studieren Informatik am KIT, und haben ein Interesse an der Entwicklung und Umsetzung von neuen Interaktionskonzepten gemeinsam mit einem Grundinteresse an Softwareverifikation.

Die Vergütung erfolgt nach den üblichen Sätzen für studentische Hilfskräfte.

Kontakt

Bei Interesse kontaktieren Sie bitte Mattias Ulbrich für ein unverbindliches Informationsgespräch.