Vorlesung: Modellprüfung - Beweiser und Algorithmen - Details

Vorlesung: Modellprüfung - Beweiser und Algorithmen - Details

Sie sind nicht in Stud.IP angemeldet.

Allgemeine Informationen

Veranstaltungsname Vorlesung: Modellprüfung - Beweiser und Algorithmen
Untertitel Modul: Modellprüfung - Beweiser und Algorithmen
Veranstaltungsnummer lv1979_S21
Semester SoSe 21
Aktuelle Anzahl der Teilnehmenden 56
Heimat-Einrichtung E-13 Eingebettete Systeme
Veranstaltungstyp Vorlesung in der Kategorie Lehre
Voraussetzungen Grundlegende Kenntnisse zu Datenstrukturen und Algorithmen
Leistungsnachweis
Mündliche Prüfung
ECTS-Punkte 6

Räume und Zeiten

Keine Raumangabe

Kommentar/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

Anmelderegeln

Diese Veranstaltung gehört zum Anmeldeset "Anmeldung gesperrt (global)".
Erzeugt durch Migration 128 13:45:31 03.09.2014
Folgende Regeln gelten für die Anmeldung:
  • Die Anmeldung ist gesperrt.