If you are interested in completing a bachelor's or master's thesis at the Chair of Verification of Complex Systems, please feel free to contact us by email at paula.herber@uni-due.de. The following list provides examples of potential thesis topics. We will be happy to advise you on which topic might be a good fit for your interests and background.

In recent years, we have developed various techniques for the formalization, verification, and analysis of embedded and cyber-physical systems. We regularly offer bachelor's and master's theses in this area. To apply and evaluate our techniques, we use SystemC and Simulink as example system description languages. Both languages originate in industrial practice.

SystemC is a modeling language developed by an industry consortium for hardware/software co-design. It is implemented as a C++ library and extends C++ with constructs for describing hardware-related concepts such as time, reactivity, and concurrency. SystemC enables integrated hardware/software systems to be modeled and simulated at different levels of abstraction throughout the entire design process.

MATLAB/Simulink is a dataflow- and signal-flow-oriented modeling language for the modeling and simulation of complex dynamic systems. Simulink extends traditional block diagrams, in which connecting signals can be either continuous or discrete, and blocks implement complex mathematical functions such as integrators, sine functions, and transformation functions. This makes it possible to model complex systems of differential and difference equations.

• Automated Test Generation for comparing Simulink with a generated SHA model
• Verification of Autonomous Cyber-Physical Systems with Simulink2dL and KeYmaera X: A Case Study
• Beyond Safety: Analyzing Performance and Resilience with Simulink2SHA
• Optimized Transformation from Simulink to dL: A Case Study
• Information Flow Analysis for Timed, Concurrent Systems modeled in SystemC: A Case Study
• Modeling FreeRTOS applications with Uppaal Timed Automata: A Case Study
• Formal Verification of RTOS-based Software: A Literature Study
• Safe Reinforcement Learning: A Literature Study

• Optimized Transformation from Simulink to dL
• Learning Contracts for Autonomous Hybrid Systems using Symbolic AI
• Automata Learning for Simulink2SHA
• Automated Invariant Generation for Scalable Verification of Preemptive RTOS Applications 
• Deriving Run-time Monitors from Deductive Verification in RTOS based Applications 
• Automated Transformation from Simulink into the OCRA Verification Framework
• Automated Transformation of FreeRTOS Applications into Uppaal Timed Automata