Lecture "Formal Verification of Software"

Vorlesung "Formale Verifikation von Software"

4.1.12 V2/V4 c CV c In(KITE,ST) 25.-30. KW

News

29.07.05: Ich bitte alle Hörer der Vorlesung (die das noch nicht gemacht haben), diesen Fragebogen auszufüllen und mir (anonym) zukommen zu lassen. Vielen Dank!
28.07.05: Link zum Together Control Center für Windows, das sich mit dem Schlüssel von der CD öffnen lässt, findet sich auf: Together Installation mit Key.
27.07.05: Restliche Folien stehen zur Verfügung.
26.07.05: Key-Syntax
24.07.05: Befragung zum Kurs.
21.07.05: Beschreibung der Together Installation mit Key.
19.07.05: Folien zum Thema Object Constraint Language zur Verfügung.
13.07.05: Kleine (korrigierte) Regelübersicht.
13.07.05: Übungen Aussagen und Prädikatenlogik. Und dynamische Logik.
11.07.05: Folien zum Thema Dynamische Logik für Java stehen zur Verfügung.
05.07.05: Installation von KeY auf einem Rechner mit Java 5.0 (Ursache, warum es unter WinXP nicht läuft)
01.07.05: Interessanter Artikel über Formale Verifikation auf Spiegel Online
01.07.05: Noch eine kleine Korrektur der Uhrzeit: die Vorlesung beginnt jeweils um 12:25 Uhr.
22.06.05: Ab sofort beginnt die Vorlesung jeweils um 12:30 Uhr.
22.06.05: Weitere Folien zu den Themen Aussagen- und Prädikatenlogik, Modallogik und Dynamische Logik stehen zur Verfügung.
22.06.05: Die Folien zur 1. Vorlesung am 21.06. stehen zur Verfügung.

Earlier News

Overview

The lecture gives an introduction to methods for deductive verification of software. Such methods allow to formally prove that an implementation satisfies its specification. Topics are:

Why verification?
Advantages and disadvantage. Costs and gains.
Basics of deductive program verification:
Hoare Logic and Dynamic Logic
Deductive verification of object-oriented programming languages
(using Java as an example)

The verification techniques will be demonstrated in the lecture using the KeY System (see www.key-project.org).

Die Vorlesung wendet sich an Studenten im Hauptstudium, und zwar gleichermaßen in den beiden Vertiefungsrichtungen "Künstliche Intelligenz" und "Softwaretechnik".

Slides

01intro.pdf - Introduction (22.06.05)
02logic.pdf - Propositional and Predicate Logic
03modalLogic.pdf - Modal Logic
04dynamicLogic.pdf - Dynamic Logic
05javaDL.pdf - Dynamic Logic for Java
06OCL.pdf - Object Constraint Language
07AbruptTermination.pdf - Handling Abrupt Termination in JavaDL
08MethodInvocation.pdf - Handling Method Invocation in JavaDL
09Integer.pdf - Handling Integer Data Types in JavaDL
10ModifiesClause.pdf - Modifies Clauses in OCL Specifications
11WrapUp.pdf - Conclusions

Times

Tuesdays, 12:30 Uhr s.t., room B016
Thursdays, 12:30 Uhr s.t., room B016

This is a twice-weekly lecture, starting on Tuesday, June 21, ending on Thursday, July 28.

Bernhard Beckert