|
Instructors: Prof. Dr. rer. nat. Reiner Hähnle
Event type:
Integrated Course
Org-unit: Dept. 20 - Computer Science
Displayed in timetable as:
FSAV
Subject:
Crediting for:
Hours per week:
4
Language of instruction:
Englisch
Min. | Max. participants:
- | -
Course Contents:
In this lecture we focus on the formal specification and deductive verification of object-oriented software.
The course covers advanced topics like:
* specification of interfaces and classes using queries, ghost fields and model fields
* the framing problem: static and dynamic framing
* program logic and calculus
* modular verification (e.g., verification of the correctness of specified frames and how to exploit framing properties)
* specification and verification of (recursive) methods, loops
* automated loop invariant/method contract generation
The course focuses on sequential programs, but current approaches on deductive verification of concurrent programs will be discussed as well.
For almost all topics tool support is available and will be demonstrated.
Preconditions:
Basic knowledge in first-order logic
Content of the lectures:
Formale Grundlagen der Informatik 2 und 3
(or similar)
|
