General

This course is offered simultaneously for the master program "Computer Science" and for the master program "Computational Mathematics". It gives a survey on the use of formal methods for the development of reliable software. More specifically, we deal with

• specifying sequential programs and concurrent systems,
• computer-supported verification,
• extended static checking,
• model checking.

The course consists of two parts:

1. a lecture part where the fundamental issues of the field are taught, and
2. an exercise part where practical skills are trained using freely available software tools.

The grading of the course will be based on a couple of exercises and a final exam. 

You have to create an account in this Moodle instance (using your jku.at email address) and self-register as a course participant (link "Enrol me in this course" at the top). You are then able to submit your assignments; furthermore, you receive per email all messages posted in the "Announcements" forum and may yourself post messages in the "Questions and Answers" forum.