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:

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.

Software

• RISC ProofNavigator
  
• Java Modeling Language (JML)
• Extended Static Checking for Java (ESC/Java2)
  
• ESC/Java2 needs Java 1.4.2, it does not work with Java 1.5!
  
• KeY Verification Environment
  
• Spin Model Checker

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