Formal Methods in Software Development (326.053, SS 2006)

Time: Thursday, 8:30-11:45.
Room: P 215.
Start: March 9.

Exam: July 6, 10:00-11:30, P215.

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,
• proof-carrying code.

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.

---

To take part in the course, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.

Exercises
A couple of exercises are distributed throughout the course (partially theoretical, partial practical using the presented software).

• Exercise 1 (April 3): exercise1.pvs
• Exercise 2 (April 27)
• Exercise 3 (May 11): arrays.pvs
• Exercise 4 (June 1)
• Exercise 5 (July 6)
  

Exercise Grades (password protected)