RISC » FormalMethods05
 
 
Topic outline
 
Formal Methods in Software Development (326.053, SS 2005)
Time: Thursday, 8:30-11:45
Room: KHG II
Start: March 10

Final Exam: the written exam will take place on Wednesday, October 12 , 17:15-18:45 in T211. No material is allowed, please do not forget your Kepler identity card.

Questions will focus on the theoretical background (Hoare calculus, predicate transformers, concurrency/model checking) and on small practical exercises (JML specifications, verifications of small code sniplets, modeling of and reasoning about small concurrent systems).

To take part in the course, you have to register in the KUSSS system.

Please also register in Moodle ("Login" at the upper right corner) such that you will receive per email all announcements that I post in the "News Forum". You may use the "Discussion Forum" for your own purpose.

Please note the changed lecture rooms (see the calendar and the announcement in the "Discussion Forum").

Forum News forum
Forum Discussion Forum
 
1
Contents and Organization

This course gives a survey on the use of formal methods for the development of reliable software. More specifically, we will deal with

  • program specification,
  • extended static checking,
  • model checking,
  • computer-supported proving,
  • 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.

Resource Introduction
Resource Introduction (4 on 1)
Resource Example Programs
Resource How to Use the Course Software at RISC

2
Program Specification

Here we deal with the Java Modeling Language (JML).

Course Presentations

Background Material

Download JML Tools (local copy) (please note that the tools only work with Java 1.4.2, not with Java 5).

Resource How to Use JML at RISC
Resource Local File Copies

3
Extended Static Checking

Here we deal with the ESC/Java2 Extended Static Checker for Java.

Course Presentations

Background Material

Download ESC/Java2 (local copy) (please note that ESC/Java2 only works with Java 1.4.2, not with Java 5).

Resource How to Use ESC/Java2 at RISC
Resource Local File Copies

4
Model Checking

Here we deal with the Spin model checker.

Course Presentations

Background Material

See also the course Systemtheory 2: Model Checking given by Prof. Armin Biere of the Institute for Formal Methods and Verification.

Download Spin (local copy)

Resource How to Use Spin at RISC
Resource Local File Copies

5
Computer-Supported Proving

Here we deal with the PVS Specification and Verification System.

Course Presentations

Background Material

Download PVS for Linux
(local copy: linux executable, system, libraries).

Resource How to Use PVS at RISC
Resource Local File Copies

6
Proof-Carrying Code
Applying formal methods in a distributed world

This part is given by Hans-Wolfgang Loidl who works in the MRG (Mobile Resource Guarantees) project at the LMU university in Munich.

  1. General PCC
    1. Motivation
    2. Basic Concepts
    3. Main challenges
    4. Components of the PCC Architecture
    5. An Example
  2. Concrete infrastructures
    1. Details of PCC infrastructures
    2. CCured
    3. ConCert/Hemlock
    4. Foundational PCC
    5. Other relevant projects
  3. PCC for resources
    1. MRG: PCC for Resources
    2. Camelot: Our High-level Language
    3. Space Inference
    4. Grail: Our intermediate language
    5. A Program Logic for Grail
    6. Termination Logic
    7. Heap Space Logic
    8. A PCC infrastructure for resource bounds
  4. Hands-on Session
    1. The MRG infrastructure
    2. The CCured infrastructure
    3. The Ciao infrastructure
    4. Other stuff

7
Exercises

8
Additional Material

The password for this section will be handed out in class. It is strongly forbidden to forward this password to anyone not participating in the course.