Skip to main content
HOME
www.lmu.de
Fakultät 11
UnterrichtsMitschau
Lehrfilme
UnterrichtOnline.org
Aktuelle Vorlesungen
Alle Vorlesungen
Faculties
Fakultätsübergreifende Vorlesungen
Katholisch-Theologische Fakultät (Fakultät 1)
Evangelisch-Theologische Fakultät (Fakultät 2)
Juristische Fakultät (Fakultät 3)
Fakultät für Betriebswirtschaft (Fakultät 4)
Volkswirtschaftliche Fakultät (Fakultät 5)
Medizinische Fakultät (Fakultät 7)
Tierärztliche Fakultät (Fakultät 8)
Fakultät für Geschichts- und Kunstwissenschaften (Fakultät 9)
Fakultät für Philosophie, Wissenschaftstheorie und Religionswissenschaft (Fakultät 10)
Fakultät für Psychologie und Pädagogik (Fakultät 11)
Fakultät für Kulturwissenschaften (Fakultät 12)
Fakultät für Sprach- und Literaturwissenschaften (Fakultät 13)
Sozialwissenschaftliche Fakultät (Fakultät 15)
Fakultät für Mathematik, Informatik und Statistik (Fakultät 16)
Fakultät für Physik (Fakultät 17)
Fakultät für Chemie und Pharmazie (Fakultät 18)
Fakultät für Biologie (Fakultät 19)
Fakultät für Geowissenschaften (Fakultät 20)
Seniorenstudium
Tutorials
FAQs
Formale Spezifikation und Verifikation
18. Programmlogik
(00:00:00)
>
Präsentation
(00:01:37)
>
Programmlogik
Date:
01.07.2015
Lecturer:
Prof. Dr. Martin Hofmann
17. Vollständigkeit der Hoare-Logik
(00:00:00)
>
Wiederholung
Date:
29.06.2015
Lecturer:
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
Date:
24.06.2015
Lecturer:
Prof. Dr. Martin Hofmann
15. Typ- und Effektsyteme: Exceptions und Referenzen
Date:
22.06.2015
Lecturer:
Prof. Dr. Martin Hofmann
14. Typ- und Effektsysteme
(00:00:00)
>
Funktionale Sprache
(00:31:16)
>
Typinferenz
Date:
17.06.2015
Lecturer:
Prof. Dr. Martin Hofmann
13. Programmanalyse und Typsysteme.
Date:
08.06.2015
Lecturer:
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
Date:
03.06.2015
Lecturer:
Prof. Dr. Martin Hofmann
11. Zusammenfassung Kapitel 2; Programmanalyse: Motivation und Einführung
Date:
01.06.2015
Lecturer:
Prof. Dr. Martin Hofmann
10. Symbolisches Model-Checking
(00:00:00)
>
Das Alternating Bit Protokoll
(00:35:56)
>
Symbolisches Model-Checking
Date:
27.05.2015
Lecturer:
Prof. Dr. Martin Hofmann
9. Alternating bit protocol
(00:00:00)
>
Das Alternating Bit Protokoll
Date:
18.05.2015
Lecturer:
Prof. Dr. Martin Hofmann
8. Das System SMV
(00:00:00)
>
Das System SMV
(01:07:20)
>
Temporallogik und Model Checking Fairness
Date:
13.05.2015
Lecturer:
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
Date:
11.05.2015
Lecturer:
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
Date:
29.04.2015
Lecturer:
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
Date:
27.04.2015
Lecturer:
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
Date:
22.04.2015
Lecturers:
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
Date:
20.04.2015
Lecturer:
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
Date:
15.04.2015
Lecturer:
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
Date:
13.04.2015
Lecturer:
Prof. Dr. Martin Hofmann
RSS-Feed abonnieren:
