(KV3/Software Engineering: 326.013, KV4/Computer Mathematics: 326.053)
Time: Friday, 8:30-11:45.
Room: T 111.
Start: October 5, 2012.
Important: To take part in the course, you have to enrol in the KUSSS system. The course is offered simultaneously as
- KV3/326.013 (for the master program "Software Engineering") and
- KV4/326.053 (for the master program "Computer Mathematics").
Please make sure to enrol for the course intended for your degree program.
This course 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.
Furthermore, a guest lecture by Mykola Nikitchenko (Taras Shevchenko National University of Kyiv) will give an introduction to
- compositional approach for program specification and verification.
The course consists of two parts:
- a lecture part where the fundamental issues of the field are taught, and
- 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.
Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the Announcements forum and may yourself post messages in the Questions and Answers forum.