| |
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.
| 
|
