| |
Formal Methods in Software Development (326.053, SS 2007)
Time: Thursday, 8:30-11:45.
Room: T 911.
Start: March 8.
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:
- 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.
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.
| |
| 4 |
Exam
The final exam will take place in written form on Tuesday, July 10, 8:30-10:00 in T112. No materials are allowed; don't forget to bring your student id card with you. The exam will focus on small examples demonstrating your basic understanding of and practical proficiency with the following topics: - Hoare calculus and weakest precondition reasoning.
- JML and extended static checking.
- Modeling, specifying, and verifying concurrent systems.
- Model checking, Proof-Carrying Code.
| 
|
