Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation

Vorlesungsbegleitendes Forschungspraktikum
im Wintersemester 2026/27

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich,

Typ:	Praktikum
Zielgruppe:	Master Informatik
Umfang:	3 Leistungspunkte oder 5 Leistungspunkte (3 Praktikum + 2 Schlüsselqualifikation)
Ort:	n.V.
Veranstaltungs-Nr.:	2400049

Zur Seite der Vorlesung

Inhalt

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen innerhalb der ersten Woche bewerben können (die Plätze sind begrenzt!). Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität der Forschungsgruppe und trägt zu deren Erfolg bei.

Beispiele für solche Forschungsaktivitäten sind etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums auf drei bis fünf Seiten dokumentiert, sowie zum letzten Vorlesungstermin im Rahmen eines Kolloquiums in jeweils etwa 10 bis 15 Minuten präsentiert und in einer anschließenden Fragerunde diskutiert.

Qualifikationsziele

Einen Forschungsansatz und die eigene Forschungs(teil-)aufgabe verstehen, begründen, bewerten und einordnen können
Aus der Aufgabenbeschreibung konkrete Arbeitsschritte entwickeln können
In dem Forschungsbereich des Projekts wissenschaftlich arbeiten können
Die für das Projekt relevanten inhaltlichen Grundlagen kennen, einsetzen und die Relevanz für die Fragestellung bewerten können
Forschungsergebnisse dokumentieren, zusammenfassen und präsentieren, sowie diskutieren können

Methodische Begleitveranstaltungen

Das Forschungspraktikum kann, wenn gewünscht, um Methodenveranstaltungen als SQ-Leistungen ergänzt werden. Die Verfügbarkeit dieses Angebots ist beschränkt durch die Kapazitäten des HoCs.

Neben der Forschungsarbeit umfasst das Praktikum auch die folgenden mit der Projektarbeit verzahnten methodischen Veranstaltungen im Rahmen von zwei Leistungspunkten (LP), die im Rahmen des Forschungspraktikums als Schlüsselqualifikationsleistungen zu besuchen sind:

Literaturrechereche und Zitieren (2,0 Stunden)
Projektmanagementworkshop (7,0 Stunden)
Präsentationsworkshop (8,0 Stunden)
Erkenntnistheorie (1,5 Stunden)
Wissenschaftstheorie (1,5 Stunden)
Workshop zum Aufstellen einer Forschungsfrage (3,0 Stunden)
Schreiben von Forschungsanträgen (1,5 Stunden)
Experimentaldesign (1,5 Stunden)

Die Workshops zu Projektmanagement und Präsentationen finden in Kooperation mit dem House of Competence (HoC) statt. Alle Veranstaltungen sind gezielt auf Forschungsprojekte im Bereich der Informatik ausgerichtet. Die Termine der Veranstaltungen werden zu Vorlesungsbeginn bekanntgegeben.

Themen

Die Themen werden zu Beginn der Vorlesung vorgestellt. Zudem sind wir offen für Themenvorschläge, die im Zusammenhang zur Vorlesung bzw. zur Forschung unserer Forschungsgruppe stehen. Beispiele hierfür sind Forschungsaktivitäten wie etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation ausgewählter formaler Methoden (u.ä.). An dieser Stelle werden wir vor Beginn der Vorlesung eine Auswahl geplanter Themen auflisten. Bei Fragen hierzu können Sie sich bereits im Vorfeld bei den genannten Ansprechpersonen melden. Gern gesehen sind auch Initiativanfragen zu Themengebieten unserer Forschungsgruppe.

Teaching Coding Agents to use KeY for Reviewing
Betreuung: Alexander Weigl

Coding agents play a central role in the development of software systems, e.g., for reviewing pull requests. It is a pity that coding agents are not yet able to use KeY to review JML specifications or to provide formally verified code reviews.

In this thesis, you will develop review scenarios in which KeY support is beneficial and integrate KeY into the workflow of coding agents via skill descriptions and MCP. Using AI agents for coding is allowed. The written report and the presentation must be done manually.
Record Patterns in KeY: Closing a completeness gap
Betreuung: Alexander Weigl

With KeY 3.0, KeY gained the ability to parse Java 25 code, but this does not mean that the calculus can handle every syntax construct correctly. One gap is record patterns in instanceof expressions, e.g., p instanceof Point(int x, int y) && x > 0.

In this thesis, you will develop a concept for record patterns, investigate the Java semantics in depth, create calculus rules, extend KeY's code where necessary, and conclude with a test bed of provable and unprovable examples. Using AI agents for coding is allowed. The written report and the presentation must be done manually.
VerifyThis – Verification Challenges with KeY and AI
Betreuung: Wolfram Pfeifer
The verification competition VerifyThis proposes interesting intricate programming puzzles as verification challenges. Quite a number of them do not have a published solution in KeY. This FP should evaluate a new scripting mechanism in KeY, and see how many challenges can be solved by adding scripts. Potentially, the script architecture should be adapted or improved based on experiences gained in this FP.
Robust synthesis of models
Betreuung: Shobhit Singh

In model-driven engineering, models (attributed typed graphs) must stay consistent with respect to a consistency relation. There is some literature on synthesizing a model given the relation and the other model, but they assume that the other model is complete. We look at the case in which both models are partial.

In this FP, you will formalise this problem for attributed typed graphs with holes over bounded domains as a game over two graphs, and implement a counterexample-guided synthesis algorithm that finds completions of the graphs.
Verification of Reaction in Isabelle/HOL Case-Study
Betreuung: Terru Stübinger
The Vitruv Tool for Multi Model-Driven system development uses a the domain-specific Reactions language to express model updates which should be applied after each development step, to ensoure that consistency between all models in the development process is maintained. Additionally, recently Vitruv gained support for declarative consistency specifications, which raises the question if declarative consistency specification and output of a Reaction agree. This FP would, via a case study, investigate how one could give a formal proof of such a Reaction's correctness.
Previous experience with Isabelle is required.
Explainable Bounded Program Verification
Betreuung: Tianhai Liu

Bounded program verification translates program behavior and verification properties into logical constraints that can be checked by SAT or SMT solvers. In addition to bounding loop iterations, bounded program verification techniques may restrict integer bit-widths and the number of object instances.

Existing bounded model checking tools, such as CBMC, can already generate counterexample traces. However, interpreting these traces and understanding the underlying causes of violations can be challenging.

This project investigates how counterexample traces can be transformed into understandable natural-language explanations, potentially using large language models (LLMs). A particular challenge is ensuring that generated explanations are faithful to the traces and do not introduce unsupported claims. Students will explore methods for generating and validating such explanations and evaluate their correctness and usefulness on selected verification examples.
Formal Modeling and Verification of Dynamic Component-Based Systems Using Networks of Timed Automata
Betreuung: Tianhai Liu

Dynamic component-based systems allow software components and services to be registered, removed, and replaced during runtime. These operations introduce complex interactions between component lifecycles, service discovery, and consumer behavior.

The project investigates how such systems and their time-based behaviors can be represented using networks of timed automata and verified with, for example, UPPAAL. Students will develop formal models of component lifecycle transitions,service registration and discovery, and dynamic service binding. They will identify and formalise relevant safety, liveness, and timing properties to detect potential inconsistency.

The possible outcomes include reusable modelling pattern(s), a case study, and an evaluation of the approach.

Ansprechperson