Willkommen zur Webseite ...

... der weiterführenden Vorlesung "Spezifikation und Verifikation von Software".

Neuigkeiten

Die Vorlesung am Do. 2. Dezember fällt aus!

Termine

Montags, 15:45 - 17:15 Uhr
Donnerstags, 15.45 - 17:15 Uhr
jeweils im Raum 131, Geb. 50.34
Details zu den Terminen
   

Vorlesungsskriptum

compressed pdf-file - uncompressed pdf-file

Zusätzliche Links

Praktikumsseite

Vorlesungsfolien

  1. Einführung (Organisatorisches, Inhaltsübersicht): bildschirm - druck
    Vorlesung am 18.10.10
  2. Rodin Demo
    Einführung in EventB: bildschirm - druck
    Vorlesung am 21.10.10
  3. Einführung in EventB (Fortsetzung und Ende)
    Die Mathematische Sprache von EventB: bildschirm - druck
    Vorlesung am 25.10.10
  4. Die Mathematische Sprache von EventB (Fortsetzung)
    Vorlesung am 28.10.10
  5. Die Mathematische Sprache von EventB (Fortsetzung und Ende)
    Theorie der Verfeinerung in EventB: bildschirm - druck
    Vorlesung am 04.11.10
  6. Theorie der Verfeinerung in EventB (Fortsetzung und Ende)
    Einführung in JML bildschirm - druck
    Vorlesung am 08.11.10
  7. Einführung in JML (Fortsetzung und Ende)
    Semantik von JML bildschirm - druck
    Vorlesung am 11.11.10
  8. Semantik von JML (Fortsetzung und Ende)
    Vorlesung am 15.11.10
  9. Typisierte Logik erster Stufe
    bildschirm - druck
    Vorlesung am 18.11.10
  10. Typisierte Logik erster Stufe (Fortsetzung und Ende)
    Vorlesung am 22.11.10
  11. Motivation für Dynamische Logik
    Folien:  bildschirm - druck
    Java Programme:  RussM.java - RussMTerm.java
    Vorlesung am 25.11.10
  12. Einführung in Dynamische Logik
    Folien:   bildschirm - druck
    Vorlesung am 29.11.10
  13. Einführung in Dynamische Logik (Fortsetzung und Ende)
    Java Programm:  Swap.java
    KeY Eingabedateien:   swap.key - term.key
    Dynamische Logik für Java
    bildschirm - druck
    Vorlesung am 06.12.10
  14. Dynamische Logik für Java (Fortsetzung und Ende)
    KeY Eingabedateien:   quantifiedUpdate.key - exceptions.key - expressions.key
               method2.key - alias.key - alias2.key - Person.java
    Vorlesung am 09.12.10
  15. Von JML zu Beweisverpflichtungen
    bildschirm - druck
    Vorlesung am 13.12.10
  16. Verifikation von Schleifen
    Folien:   bildschirm - druck
    weakest precondition Kalkül
    Folien:   bildschirm - druck
    Vorlesung am 16.12.10
  17. ESCJava
    Folien:   bildschirm - druck
    Vorlesung am 20.12.10
  18. Sequentielle Algorithmen
    Folien:   bildschirm - druck
    Vorlesung am 10.01.11
  19. Sequentielle Algorithmen (Fortsetzung
    Vorlesungsevaluierung
    Vorlesung am 13.01.11
  20. Abstract State Machines (ASM)
    Folien:   bildschirm - druck
    Zusammenfassung
    Folien:   bildschirm - druck
    Vorlesung am 20.01.11
  21. Vorlesungsende

Java Programme und KeY Eingabedateien

Alte Webseiten

2009

Kontakt

E-Mail · Sprechstunde