Jun.-Prof. Dr. Bernhard Beckert
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.
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.