| |
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.
| |
| 1 |
Contents
This is the tentative syllabus of the course which is going to be augmented by the course materials (slides and papers).
- Computer programs/systems as subjects of reasoning.
- Specifying and Verifying Sequential Programs
- Specifying and Verifying Java Programs
- Specifiying and Verifying Concurrent Systems
- Proof-Carrying Code (PCC)
Proof-carrying-code (PCC) is a software mechanism that allows a host system to determine with certainty that it is safe to execute a program supplied by an untrusted source. This is achieved by attaching a condensed version of a formal proof to the program. In this part of the course we will examine the principles of PCC, explore different variants in the design of a PCC infrastructure, and take a closer look at some selected PCC infrastructures.
The structure of this part of the course is as follows:
- Motivation
- Basic Concepts
- An Example: CCured
- Components of the PCC Architecture
- Main challenges
- PCC for Resources
- Certificate Generation
- Summary
Restricted Area
The password to this area is handed out in class.
| 
|
| 2 |
Software
The following software is used in the course:
All of this software is freely available under Linux (see also the information for MS Windows Users). You can simply use the software installation in the RISC Environment (supported and recommended) or install and run it on your own PC (at your own risk, I cannot give installation support).
|
|
| 3 |
|
|
| 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.
|
|
