Marwan Mostafa

M.Sc.
Research Assistant

Contact

Marwan Mostafa, M.Sc.
E-6 Elektrische Energietechnik
  • Elektrische Energietechnik
Office Hours
nach Vereinbarung/ by appointment
Harburger Schloßstraße 36,
21079 Hamburg
Building HS36, Room C3 0.013
Phone: +49 40 42878 4097
Logo

Research Project

iNeP
Integrated network planning for the electricity, gas and heat sectors

iNeP

Integrated network planning for the electricity, gas and heat sectors

Federal Ministry for Economic Affairs and Climate Action (BMWK); Duration: 2021 to 2026

Publications

TUHH Open Research (TORE)

2023

2022

2021

Courses

Stud.IP
zur Veranstaltung in Stud.IP Studip_icon
Modellprüfung - Beweiser und Algorithmen (VL)
Untertitel:
Diese Lehrveranstaltung ist Teil des Moduls: Modellprüfung - Beweiser und Algorithmen
Semester:
SoSe 23
Veranstaltungstyp:
Vorlesung (Lehre)
Veranstaltungsnummer:
lv1979_s23
DozentIn:
Prof. Dr.-Ing. Görschwin Fey, M. Sc. Lutz Schammer
Beschreibung:

Correctness is a major concern in embedded systems. Model checking can fully automatically proof formal properties about digital hardware or software. Such properties are given in temporal logic, e.g., to prove "No two orthogonal traffic lights will ever be green."

And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?

But what are the limitations of model checking?
How are the models generated from a given design?
The lecture will answer these questions. Open source tools will be used to gather a practical experience.

Among other topics, the lecture will consider the following topics:

  • Modelling digital Hardware, Software, and Cyber Physical Systems

  • Data structures, decision procedures and proof engines

    • Binary Decision Diagrams

    • And-Inverter-Graphs

    • Boolean Satisfiability

    • Satisfiability Modulo Theories

  • Specification Languages

    • CTL

    • LTL

    • System Verilog Assertions

  • Algorithms for

    • Reachability Analysis

    • Symbolic CTL Checking

    • Bounded LTL-Model Checking

    • Optimizations, e.g., induction, abstraction

  • Quality assurance

Leistungsnachweis:
695 - Modellprüfung - Beweiser und Algorithmen<ul><li>695 - Modellprüfung - Beweiser und Algorithmen: mündlich</li></ul><br>m1397 - Modellprüfung - Beweiser und Algorithmen<ul><li>p1309 - Modellprüfung - Beweiser und Algorithmen: mündlich</li><li>vl360 - Verpflichtende Studienleistung Modellprüfung - Beweiser und Algorithmen - Fachtheoretisch-fachpraktische Studienleistung: Fachtheoretisch-fachpraktische Studienleistung</li></ul>
ECTS-Kreditpunkte:
3
Weitere Informationen aus Stud.IP zu dieser Veranstaltung
Heimatinstitut: Institut für Eingebettete Systeme (E-13)
In Stud.IP angemeldete Teilnehmer: 35
Anzahl der Dokumente im Stud.IP-Downloadbereich: 5

Supervised Theses

ongoing
completed

2022

  • Barthelme, J. (2022). Technisch-ökonomische Systemmodellierung und -anlayse eines urbanen Quatiers hinsichtlich des Einsatz von Wasserstoff als primärer Energieträger.