Jun.-Prof. Dr. Bernhard Beckert
The purpose of formal methods in software engineering is to ensure, with high confidence, that systems behave according to their specification. Mostly, this is done (1) using specification languages that have a formal semantics to describe the intended behaviour and (2) using logic-based techniques to formally prove that a program satisfies its specification.
This course will give a general introduction into the basic techniques of formal specification and verification and then concentrate on the specification and 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 (the book on KeY will be available to the course participants). 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.
Thu, July 5: 9.00 - 10.00 (changed!)
Thu, July 5: 12.15 - 13.45
Fri, July 6: 9.00 - 10.00
Tue, July 10: 10.15 - 11.45 Room G 409 (changed!)
Tue, July 10: 12.15 - 13.45
Thu, July 12: 8.30 - 10.00
Thu, July 12: 12.15 - 13.45
Tue, July 17: 12.15 - 13.45
Wed, July 18: 8.30 - 10.00
Wed, July 18: 12.15 - 13.45
Thu, July 19: 8.30 - 10.00
Thu, July 19: 12.15 - 13.45
There are 12 sessions of 90min. This corresponds to a regular course of 2 hours (90min) of lecture per week for an entire semester. Thus, the credit to be earned is 3.0 ECTS points.