Lecture "Formal Verification of Software"

Vorlesung "Formale Verifikation von Software"

July 24, 2006 - July 28, 2006

4.1.10 V2 c CV, In(KITE,ST) - Summer Academy

Jun.-Prof. Dr. Bernhard Beckert


News

23.07.06: The lecture starts on Monday, 24.07.06, at 16:15 in room A120. On the first day, we will probably not really get to the point where we can do practical exercises with a verification system. But please bring your laptops anyway. We will distribute CDs with the verification software for you to install.
05.05.06: If you plan to attend this lecture, then please register until June 15 via MeToo
05.05.06: See also the official Summer Academy web page for this lecture


Overview

The purpose of formal software verification is to ensure, with high confidence, that systems behave according to their specification.

This course will give a general introduction into the basic techniques of formal specification and verification and then concentrate on the deductive verification of object-oriented programs.

Participants will learn about the following topics and techniques:

We use a concrete tool to illustrate the concepts and methods that are introduced in the course: The KeY tool is an integrated tool for object-oriented design and formal verification. It is developed here in Koblenz and at the University of Karlsruhe and Chalmers University, Gothenburg. The target language of KeY is a subset of Java. KeY supports UML class diagrams, formal specification in OCL, translation from OCL into logic, and an interactive theorem prover that is used to formally verify statements about specifications and programs.



Slides


Times and Room

The course will take place in calendar week 30 (from: July 24, 2006 to: July 28, 2006) in room A 120 at the following times:

Mon, July 24: 16.00 - 20.00
Tue, July 25: 12.00 - 18.00
Wed, July 26: 16.00 - 20.00
Thu, July 27: 12.00 - 18.00
Fri, July 28: 10.00 - 14.00

This corresponds to a regular course of 2 hours of lecture per week for an entire semester. Thus, the credit to be earned is 3.0 ECTS points.


Bernhard Beckert