Universität Bremen  
  FB 3  
  Group BKB > Teaching > WS 04/05 > Deutsch

[VAK 03-604.03] Formal Methods of Software Development I


Till Mossakowski
Lutz Schröder

Mon 13:00 - 15:00 MZH 7230,
Wed 15:00 - 17:00 MZH 7250

First lecture Wednesday, October 20th, 2004

In modern software development, applications that require, for safety reasons,  a reliable, permanent and correct functioning of the product play a role of increasing importance. This course is about methods of precise specification of correctness requirements and about how these are guaranteed to hold during the whole development process. The course will be based on formal specification languages, testing tools and semi-automatic theorem provers. The implementation language will be Haskell.

Overview of the course

Slides: lect1  lect2  lect3  lect4  lect5  lect6

Isabelle Slides: Lecture 1;  the meta-logic; primitive recursion; unification and resolution; simplification

Isabelle Examples: Script for demo application of a meta-rule (in classical Isabelle -- type isabelle HOL)

Isabelle Problems: sheet 1; deliverable exercise

Haskell examples: QuickCheck examples   Queues  State Monad

Exercises: ex1  sample test cases  ex2  sample programs  ex3  sample solution  ex4   (Isabelle exercises see above)

Related lecture: Advanced techniques of functional programming (Wed 17-19h, MZH 8090)


Author: Dr. Till Mossakowski
  Group BKB 
Last updated: February 9, 2005   impressum