Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2009/10 / Spezifikation und Verifikation


Inhaltsbereich

Spezifikation und Verifikation

Vorlesung, 3-std., Mo 10-12, Do 10-12, Hofmann; Übungen 2-std., Schöpp

 


Aktuelles

  •  Die Anmeldung zur Nachholklausur am 14.4. ist nun über UniWorX möglich (bis 11.4.).

 


Inhalt

In der Vorlesung werden Spezifikationsformalismen, Konzepte der Systemmodellierung, Grundtechniken für die Automatisierung der Verifikation, Typsysteme und statische Analyse eingeführt.

 


Organisation

 


Zeit und Ort

Veranstaltung  Zeit  Ort Beginn
Vorlesung Mo, 10–12 c.t. Hörsaal B005 (Theresienstr. 39) 26.10.2009
Vorlesung Do, 10–12 c.t. Hörsaal B005 (Theresienstr. 39) 29.10.2009
Übung Fr, 10–12 c.t. Hörsaal B041 (Theresienstr. 39) 30.10.2009
Übung Fr, 12–14 c.t. Hörsaal B041 (Theresienstr. 39) 30.10.2009

Die Vorlesung findet an den folgenden Terminen statt: 26.10.09, 29.10.09, 09.11.09, 12.11.09, 16.11.09, 19.11.09, 23.11.09, 26.11.09, 30.11.09, 03.12.09, 07.12.09, 10.12.09, 14.12.09, 11.01.10, 14.01.10, 25.01.10, 28.01.10, 01.02.10, 04.02.10, 08.02.10

 


Log

Termin  Stoff Folien Sonstiges
26.10. Organisatorisches, Aussagenlogik, Beispiel: Sudoku 1-27  
29.10 Tseitin Übersetzung, Sat-Solver, DPLL-Algorithmus mit Klausellernen, Modellierung von Addierwerken 28-48  
3.11. keine Vorlesung    
5.11. keine Vorlesung    
9.11. Modellierung nebenläufiger Systeme in Aussagenlogik mit Sat-Solver. 49-51  
12.11. Wdh Peterson mit SAT Solver. BDDs Grundlegende Definitionen 51-66  
16.11. BDDs Grundalgorithmen und Implementierung, Modellierung nebenl. Systeme mit BDDs 67-79  
19.11. Wdh Mod. mit BDDs. Einf. Model-Checking CTL Syntax&Semantik 80-95  
23.11. Model-Checking Algorithmus fuer CTL 96-105  
26.11. Das System SMV 106-126  
30.11. Model Checking mit Fairness, Alternating Bit Protokoll 127-135  
3.12. ABP fertig (s.u.), Symbolisches Model-Checking, LTL, Definition Buechi-Automat 136-148  
7.12. Buechi Automaten, Model-Checking mit Buechi Automaten, SPIN, Kapitel 3 Motivation 149-163  
10.12. Programmanalyse: Reaching Definitions, Gleichungs- und Constraintbasiert. Available Expressions. 164-177  
14.12. Datenflussgleichungen, Liveness von Variablen, groesste/kleinste Loesung. Typsystem fuer Reaching Definitions 178-187  
17.12. keine Vorlesung    
21.12. keine Vorlesung    
7.1. keine Vorlesung    
11.1. Wdh. Semantische Korrektheit von Programmanalysen mit Typsystemen. Operationelle Semantik
188-192  
14.1. Wdh. Funktionale Sprache, einfaches Typsystem. Typinferenz mit Beispielen. 193-201  
18.1. keine Vorlesung    
21.1. keine Vorlesung    
25.1. Typinferenz fuer einfaches und polymorphes Typsystem. Kontrollflussanalyse (nur Motivation). 202-215  
28.1. Typsysteme fuer Kontrollflussanalyse und Seiteneffekte. Effektsystem im allgemeinen, Subtyping 216-229  
1.2. Typ- und Effektsystem fuer Exceptions, Zusammenfassung Typsysteme 230-239  
4.2. Klausurwiederholung    
8.2. Klausurwiederholung / Hoare Logik mit rekursiven Prozeduren    

 


Materialien

 


Übungen

 


Literatur

 


Klausur

 Erstklausur: Dienstag 16.2. 10–13 Uhr, Hörsaal A140 (Hauptgebäude, 1.Stock, Raumplan (Mitte oben))

  • Bearbeitungszeit: 120 Minuten
  • Die Klausur findet ohne Hilfsmittel statt. Insbesondere sind keine schriftlichen Unterlagen, keine Taschenrechner oder andere Rechner, keine Mobiltelefone oder andere Kommunikationsmittel erlaubt.
  • Erforderliche Unterlagen:
    • gültiger Immatrikulationsnachweis für dieses Semester
    • gültiger Personalausweis oder Pass mit Lichtbild
    • Schreibzeug
    • Eigenes Papier ist nicht erforderlich und darf für die Prüfung nicht benutzt werdenE
  • Ergebnis (inkl. Notenbonus)
  • Einsicht: Freitag 5.3. 14–15 Uhr, Oettingenstraße 67, Z1.09 (neu L109)

 Nachholklausur: Mittwoch 14.4. 14–17 Uhr, Hörsaal A240 (Hauptgebäude)

  • Ergebnis (inkl. Notenbonus)
  • Einsicht: Freitag 7.5. 13:15–14:15 Uhr, Oettingenstraße 67, U169

 

Artikelaktionen


Funktionsleiste