FB 3  
Group BKB > Teaching > WS 04/05 >  
[VAK 03604.03] Formal Methods of Software Development I 

Till Mossakowski Lutz Schröder K 4 SWS 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 semiautomatic theorem provers. The implementation language will be Haskell. Overview of the course
Slides: lect1 lect2 lect3 lect4 lect5 lect6 Isabelle Slides: Lecture 1; the metalogic; primitive recursion; unification and resolution; simplification Isabelle Examples: Script for demo application of a metarule (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 1719h, MZH 8090) Literature


Author: Dr. Till Mossakowski 

Group BKB 
