Formale Spezifikation und Verifikation

18. Programmlogik

(00:00:00) >: Präsentation

(00:01:37) >: Programmlogik

Datum: 01.07.2015

Dozent(in): Prof. Dr. Martin Hofmann

17. Vollständigkeit der Hoare-Logik

(00:00:00) >: Wiederholung

Datum: 29.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

16. Wiederholung: Typ- und Effektivsteme und Hoare Logik

(00:00:00) >: Typsystem für Speicherzugriffe

(00:20:12) >: Polymorphes Typsystem für Exceptions

(00:32:33) >: Programmlogik

Datum: 24.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

15. Typ- und Effektsyteme: Exceptions und Referenzen

Datum: 22.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

14. Typ- und Effektsysteme

(00:00:00) >: Funktionale Sprache

(00:31:16) >: Typinferenz

Datum: 17.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

13. Programmanalyse und Typsysteme.

Datum: 08.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

12. Constraint-basierter Analyse

(00:00:00) >: Constraint-basierte Analyse

(00:10:01) >: Weitere Analysen Verfügbare Ausdrücke

(00:23:50) >: Weitere Analysen Fixpunkttheorie

Datum: 03.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

11. Zusammenfassung Kapitel 2; Programmanalyse: Motivation und Einführung

Datum: 01.06.2015

Dozent(in): Prof. Dr. Martin Hofmann

10. Symbolisches Model-Checking

(00:00:00) >: Das Alternating Bit Protokoll

(00:35:56) >: Symbolisches Model-Checking

Datum: 27.05.2015

Dozent(in): Prof. Dr. Martin Hofmann

9. Alternating bit protocol

(00:00:00) >: Das Alternating Bit Protokoll

Datum: 18.05.2015

Dozent(in): Prof. Dr. Martin Hofmann

8. Das System SMV

(00:00:00) >: Das System SMV

(01:07:20) >: Temporallogik und Model Checking Fairness

Datum: 13.05.2015

Dozent(in): Prof. Dr. Martin Hofmann

7. Model-Checking-Algorithmen

(00:02:33) >: Wiederholung

(00:10:37) >: Mutual Exclusion Beispiel

(00:18:11) >: CTL-Model Checking

(01:13:54) >: CTL-Model Checking: State-Explosion-Problem

Datum: 11.05.2015

Dozent(in): Prof. Dr. Martin Hofmann

6. CTL, Model Checking

(00:00:00) >: Nebenläufige Systeme mit BDDs

(00:09:05) >: Iteration

(00:27:12) >: Kapitel 2 - Temporallogik und Model Checking

(00:35:13) >: Sinn der Temporallogik

(00:44:25) >: Informelle Semantik der CTL-Formeln

(01:01:58) >: Formale Semantik von CTL

(01:16:53) >: Semantik der Until-Formeln

(01:23:48) >: Äquivalenzen

Datum: 29.04.2015

Dozent(in): Ulrich Schöpp

5. BDDs

(00:00:00) >: Wiederholung

(00:04:05) >: Implementierung I

(00:12:33) >: Bibliothek BuDDy

(00:24:25) >: Lookahead Addierer mit BDDs

(00:33:53) >: Nebenläufige Systeme mit BDDs

(00:49:42) >: Semaphor mit BDDs

Datum: 27.04.2015

Dozent(in): Prof. Dr. Martin Hofmann

4. BDDs

(00:00:00) >: Wiederholung: Peterson Algorithmus

(00:03:34) >: BDDs Grundidee

(00:33:29) >: Logische Operationen auf BDDs

(00:50:58) >: Beispiel

(01:05:59) >: Existentielle Quantifizierung

Datum: 22.04.2015

Dozierende: Prof. Dr. Martin Hofmann | Ulrich Schöpp

3. Aussagenlogik

(00:00:00) >: Gleichheit von Schaltkreisen

(00:45:35) >: Modellierung nebenlläufiger Systeme

(01:06:56) >: Peterson Algorithmus

Datum: 20.04.2015

Dozent(in): Prof. Dr. Martin Hofmann

2. Konjunktive Normalform, Disjunktive Normalform

(00:00:00) >: Wiederholung

(00:27:30) >: SAT-Solver

(00:58:01) >: SAT-Solver Optimierung

(01:10:42) >: Gleichheit von Schaltkreisen

Datum: 15.04.2015

Dozent(in): Prof. Dr. Martin Hofmann

1. Organisation, Aussagenlogik: Syntax und Semantik, Modellierung von Sudoku

(00:00:00) >: Einführung

(00:01:20) >: Was ist Spezifikation?

(00:04:11) >: Was ist Verifikation?

(00:10:03) >: Inhalt

(00:18:41) >: Organisatorisches, Literatur

(00:19:48) >: Kapitel 1.Propositionale Logik

(00:20:24) >: Motivation

(00:27:55) >: Syntax und Semantik der Aussagenlogik

(00:38:05) >: Tautologien und Erfüllbarkeit

(00:51:02) >: Mengennotation und indizierte Variablen

(01:14:55) >: Normalformen: Begriffe

Datum: 13.04.2015

Dozent(in): Prof. Dr. Martin Hofmann

RSS-Feed abonnieren: